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  877  ccase  906  mpjao3dan  1239  relop  4514  poltletr  4755  tfrlemisucaccv  5974  tfr1onlemsucaccv  5990  tfrcllemsucaccv  6003  phplem3  6389  ssfilem  6410  diffitest  6421  reapmul1  7762  apsqgt0  7768  recexaplem2  7809  nnnn0addcl  8385  un0addcl  8388  un0mulcl  8389  elz2  8500  xrltso  8947  fzsplit2  9145  fzsuc2  9172  elfzp12  9192  expp1  9580  expnegap0  9581  expcllem  9584  mulexpzap  9613  expaddzap  9617  expmulzap  9619  bcpasc  9790  odd2np1  10417  dvdslcm  10595  lcmeq0  10597  lcmcl  10598  lcmneg  10600  lcmgcd  10604  rpexp1i  10677
 Copyright terms: Public domain W3C validator