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

Theorem jaodan 787
 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 707 . 2 (𝜑 → ((𝜓𝜃) → 𝜒))
65imp 123 1 ((𝜑 ∧ (𝜓𝜃)) → 𝜒)
 Colors of variables: wff set class Syntax hints:   → wi 4   ∧ wa 103   ∨ wo 698 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 699 This theorem depends on definitions:  df-bi 116 This theorem is referenced by:  mpjaodan  788  ordi  806  andi  808  dcor  920  ccase  949  mpjao3dan  1289  relop  4733  poltletr  4983  tfrlemisucaccv  6266  tfr1onlemsucaccv  6282  tfrcllemsucaccv  6295  phplem3  6792  ssfilem  6813  diffitest  6825  reapmul1  8453  apsqgt0  8459  recexaplem2  8509  nnnn0addcl  9103  un0addcl  9106  un0mulcl  9107  elz2  9218  xrltso  9685  xaddnemnf  9743  xaddnepnf  9744  fzsplit2  9934  fzsuc2  9963  elfzp12  9983  expp1  10408  expnegap0  10409  expcllem  10412  mulexpzap  10441  expaddzap  10445  expmulzap  10447  bcpasc  10622  xrltmaxsup  11136  xrmaxaddlem  11139  summodc  11262  fsumsplit  11286  fprodsplitdc  11475  ef0lem  11539  odd2np1  11745  dvdslcm  11926  lcmeq0  11928  lcmcl  11929  lcmneg  11931  lcmgcd  11935  rpexp1i  12008
 Copyright terms: Public domain W3C validator