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

Theorem jaodan 744
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 113 . . 3 (𝜑 → (𝜓𝜒))
3 jaodan.2 . . . 4 ((𝜑𝜃) → 𝜒)
43ex 113 . . 3 (𝜑 → (𝜃𝜒))
52, 4jaod 670 . 2 (𝜑 → ((𝜓𝜃) → 𝜒))
65imp 122 1 ((𝜑 ∧ (𝜓𝜃)) → 𝜒)
Colors of variables: wff set class
Syntax hints:  wi 4  wa 102  wo 662
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-io 663
This theorem depends on definitions:  df-bi 115
This theorem is referenced by:  mpjaodan  745  ordi  763  andi  765  dcor  879  ccase  908  mpjao3dan  1241  relop  4554  poltletr  4799  tfrlemisucaccv  6044  tfr1onlemsucaccv  6060  tfrcllemsucaccv  6073  phplem3  6522  ssfilem  6543  diffitest  6555  reapmul1  8013  apsqgt0  8019  recexaplem2  8060  nnnn0addcl  8636  un0addcl  8639  un0mulcl  8640  elz2  8751  xrltso  9198  fzsplit2  9396  fzsuc2  9423  elfzp12  9443  expp1  9860  expnegap0  9861  expcllem  9864  mulexpzap  9893  expaddzap  9897  expmulzap  9899  bcpasc  10070  isummo  10662  odd2np1  10748  dvdslcm  10926  lcmeq0  10928  lcmcl  10929  lcmneg  10931  lcmgcd  10935  rpexp1i  11008
  Copyright terms: Public domain W3C validator