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

Theorem jaodan 769
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 689 . 2 (𝜑 → ((𝜓𝜃) → 𝜒))
65imp 123 1 ((𝜑 ∧ (𝜓𝜃)) → 𝜒)
Colors of variables: wff set class
Syntax hints:  wi 4  wa 103  wo 680
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 681
This theorem depends on definitions:  df-bi 116
This theorem is referenced by:  mpjaodan  770  ordi  788  andi  790  dcor  902  ccase  931  mpjao3dan  1268  relop  4649  poltletr  4897  tfrlemisucaccv  6176  tfr1onlemsucaccv  6192  tfrcllemsucaccv  6205  phplem3  6701  ssfilem  6722  diffitest  6734  reapmul1  8275  apsqgt0  8281  recexaplem2  8326  nnnn0addcl  8911  un0addcl  8914  un0mulcl  8915  elz2  9026  xrltso  9475  xaddnemnf  9533  xaddnepnf  9534  fzsplit2  9723  fzsuc2  9752  elfzp12  9772  expp1  10193  expnegap0  10194  expcllem  10197  mulexpzap  10226  expaddzap  10230  expmulzap  10232  bcpasc  10405  xrltmaxsup  10918  xrmaxaddlem  10921  summodc  11044  fsumsplit  11068  ef0lem  11217  odd2np1  11418  dvdslcm  11596  lcmeq0  11598  lcmcl  11599  lcmneg  11601  lcmgcd  11605  rpexp1i  11678
  Copyright terms: Public domain W3C validator