Intuitionistic Logic Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  ILE Home  >  Th. List  >  jaodan GIF version

Theorem jaodan 710
 Description: Deduction disjoining the antecedents of two implications. (Contributed by NM, 14-Oct-2005.)
Hypotheses
Ref Expression
jaodan.1 ((𝜑𝜓) → 𝜒)
jaodan.2 ((𝜑𝜃) → 𝜒)
Assertion
Ref Expression
jaodan ((𝜑 ∧ (𝜓𝜃)) → 𝜒)

Proof of Theorem jaodan
StepHypRef Expression
1 jaodan.1 . . . 4 ((𝜑𝜓) → 𝜒)
21ex 108 . . 3 (𝜑 → (𝜓𝜒))
3 jaodan.2 . . . 4 ((𝜑𝜃) → 𝜒)
43ex 108 . . 3 (𝜑 → (𝜃𝜒))
52, 4jaod 637 . 2 (𝜑 → ((𝜓𝜃) → 𝜒))
65imp 115 1 ((𝜑 ∧ (𝜓𝜃)) → 𝜒)
 Colors of variables: wff set class Syntax hints:   → wi 4   ∧ wa 97   ∨ wo 629 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-io 630 This theorem depends on definitions:  df-bi 110 This theorem is referenced by:  mpjaodan  711  ordi  729  andi  731  dcor  843  ccase  871  mpjao3dan  1202  relop  4486  poltletr  4725  tfrlemisucaccv  5939  phplem3  6317  ssfiexmid  6336  diffitest  6344  reapmul1  7586  apsqgt0  7592  recexaplem2  7633  nnnn0addcl  8212  un0addcl  8215  un0mulcl  8216  elz2  8312  xrltso  8717  fzsplit2  8914  fzsuc2  8941  elfzp12  8961  expp1  9262  expnegap0  9263  expcllem  9266  mulexpzap  9295  expaddzap  9299  expmulzap  9301
 Copyright terms: Public domain W3C validator