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

Theorem jaodan 721
 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 112 . . 3
3 jaodan.2 . . . 4
43ex 112 . . 3
52, 4jaod 647 . 2
65imp 119 1
 Colors of variables: wff set class Syntax hints:   wi 4   wa 101   wo 639 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 103  ax-ia2 104  ax-ia3 105  ax-io 640 This theorem depends on definitions:  df-bi 114 This theorem is referenced by:  mpjaodan  722  ordi  740  andi  742  dcor  854  ccase  882  mpjao3dan  1213  relop  4513  poltletr  4752  tfrlemisucaccv  5969  phplem3  6347  ssfiexmid  6366  diffitest  6374  reapmul1  7659  apsqgt0  7665  recexaplem2  7706  nnnn0addcl  8268  un0addcl  8271  un0mulcl  8272  elz2  8369  xrltso  8817  fzsplit2  9015  fzsuc2  9042  elfzp12  9062  expp1  9426  expnegap0  9427  expcllem  9430  mulexpzap  9459  expaddzap  9463  expmulzap  9465  bcpasc  9633  odd2np1  10183
 Copyright terms: Public domain W3C validator