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

Theorem jaodan 709
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 636 . 2
65imp 115 1
Colors of variables: wff set class
Syntax hints:   wi 4   wa 97   wo 628
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 629
This theorem depends on definitions:  df-bi 110
This theorem is referenced by:  mpjaodan  710  ordi  728  andi  730  dcor  842  ccase  870  mpjao3dan  1201  relop  4429  poltletr  4668  tfrlemisucaccv  5880  ssfiexmid  6254  reapmul1  7379  apsqgt0  7385  recexaplem2  7415  nnnn0addcl  7988  un0addcl  7991  un0mulcl  7992  elz2  8088  xrltso  8487  fzsplit2  8684  fzsuc2  8711  elfzp12  8731  expp1  8916  expnegap0  8917  expcllem  8920  mulexpzap  8949  expaddzap  8953  expmulzap  8955
  Copyright terms: Public domain W3C validator