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

Theorem jaod 707
Description: Deduction disjoining the antecedents of two implications. (Contributed by NM, 18-Aug-1994.) (Revised by NM, 4-Apr-2013.)
Hypotheses
Ref Expression
jaod.1  |-  ( ph  ->  ( ps  ->  ch ) )
jaod.2  |-  ( ph  ->  ( th  ->  ch ) )
Assertion
Ref Expression
jaod  |-  ( ph  ->  ( ( ps  \/  th )  ->  ch )
)

Proof of Theorem jaod
StepHypRef Expression
1 jaod.1 . . . 4  |-  ( ph  ->  ( ps  ->  ch ) )
21com12 30 . . 3  |-  ( ps 
->  ( ph  ->  ch ) )
3 jaod.2 . . . 4  |-  ( ph  ->  ( th  ->  ch ) )
43com12 30 . . 3  |-  ( th 
->  ( ph  ->  ch ) )
52, 4jaoi 706 . 2  |-  ( ( ps  \/  th )  ->  ( ph  ->  ch ) )
65com12 30 1  |-  ( ph  ->  ( ( ps  \/  th )  ->  ch )
)
Colors of variables: wff set class
Syntax hints:    -> wi 4    \/ wo 698
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 699
This theorem depends on definitions:  df-bi 116
This theorem is referenced by:  mpjaod  708  jaao  709  orel2  716  pm2.621  737  mtord  773  jaodan  787  pm2.63  790  pm2.74  797  dedlema  954  dedlemb  955  oplem1  960  opthpr  3735  trsucss  4383  ordsucim  4459  onsucelsucr  4467  0elnn  4578  xpsspw  4698  relop  4736  fununi  5238  poxp  6179  nntri1  6443  nnsseleq  6448  nnmordi  6463  nnaordex  6474  nnm00  6476  swoord2  6510  nneneq  6802  exmidonfinlem  7128  elni2  7234  prubl  7406  distrlem4prl  7504  distrlem4pru  7505  ltxrlt  7943  recexre  8453  remulext1  8474  mulext1  8487  un0addcl  9123  un0mulcl  9124  elnnz  9177  zleloe  9214  zindd  9282  uzsplit  9994  fzm1  10002  expcl2lemap  10431  expnegzap  10453  expaddzap  10463  expmulzap  10465  nn0opthd  10596  facdiv  10612  facwordi  10614  bcpasc  10640  recvguniq  10895  absexpzap  10980  maxabslemval  11108  xrmaxiflemval  11147  sumrbdclem  11274  summodc  11280  zsumdc  11281  prodrbdclem  11468  zproddc  11476  prodssdc  11486  fprodcl2lem  11502  fprodsplitsn  11530  ordvdsmul  11727  gcdaddm  11867  lcmdvds  11955  dvdsprime  11998  prmdvdsexpr  12024  prmfac1  12026  unct  12171  baspartn  12448  reopnap  12938  coseq0q4123  13155  decidin  13371  bj-charfun  13382  bj-nntrans  13526  bj-nnelirr  13528  bj-findis  13554  exmid1stab  13572  triap  13600
  Copyright terms: Public domain W3C validator