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

Theorem jaodan 710
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 108 . . 3 (𝜑 → (𝜓𝜒))
3 jaodan.2 . . . 4 ((𝜑𝜃) → 𝜒)
43ex 108 . . 3 (𝜑 → (𝜃𝜒))
52, 4jaod 637 . 2 (𝜑 → ((𝜓𝜃) → 𝜒))
65imp 115 1 ((𝜑 ∧ (𝜓𝜃)) → 𝜒)
Colors of variables: wff set class
Syntax hints:  wi 4  wa 97  wo 629
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-io 630
This theorem depends on definitions:  df-bi 110
This theorem is referenced by:  mpjaodan  711  ordi  729  andi  731  dcor  843  ccase  871  mpjao3dan  1202  relop  4486  poltletr  4725  tfrlemisucaccv  5939  phplem3  6317  ssfiexmid  6336  diffitest  6344  reapmul1  7584  apsqgt0  7590  recexaplem2  7631  nnnn0addcl  8210  un0addcl  8213  un0mulcl  8214  elz2  8310  xrltso  8715  fzsplit2  8912  fzsuc2  8939  elfzp12  8959  expp1  9236  expnegap0  9237  expcllem  9240  mulexpzap  9269  expaddzap  9273  expmulzap  9275
  Copyright terms: Public domain W3C validator