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

Theorem jaodan 771
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 114 . . 3 (𝜑 → (𝜓𝜒))
3 jaodan.2 . . . 4 ((𝜑𝜃) → 𝜒)
43ex 114 . . 3 (𝜑 → (𝜃𝜒))
52, 4jaod 691 . 2 (𝜑 → ((𝜓𝜃) → 𝜒))
65imp 123 1 ((𝜑 ∧ (𝜓𝜃)) → 𝜒)
Colors of variables: wff set class
Syntax hints:  wi 4  wa 103  wo 682
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 683
This theorem depends on definitions:  df-bi 116
This theorem is referenced by:  mpjaodan  772  ordi  790  andi  792  dcor  904  ccase  933  mpjao3dan  1270  relop  4659  poltletr  4909  tfrlemisucaccv  6190  tfr1onlemsucaccv  6206  tfrcllemsucaccv  6219  phplem3  6716  ssfilem  6737  diffitest  6749  reapmul1  8325  apsqgt0  8331  recexaplem2  8381  nnnn0addcl  8975  un0addcl  8978  un0mulcl  8979  elz2  9090  xrltso  9550  xaddnemnf  9608  xaddnepnf  9609  fzsplit2  9798  fzsuc2  9827  elfzp12  9847  expp1  10268  expnegap0  10269  expcllem  10272  mulexpzap  10301  expaddzap  10305  expmulzap  10307  bcpasc  10480  xrltmaxsup  10994  xrmaxaddlem  10997  summodc  11120  fsumsplit  11144  ef0lem  11293  odd2np1  11497  dvdslcm  11677  lcmeq0  11679  lcmcl  11680  lcmneg  11682  lcmgcd  11686  rpexp1i  11759
  Copyright terms: Public domain W3C validator