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

Theorem jaod 712
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 711 . 2  |-  ( ( ps  \/  th )  ->  ( ph  ->  ch ) )
65com12 30 1  |-  ( ph  ->  ( ( ps  \/  th )  ->  ch )
)
Colors of variables: wff set class
Syntax hints:    -> wi 4    \/ wo 703
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 704
This theorem depends on definitions:  df-bi 116
This theorem is referenced by:  mpjaod  713  jaao  714  orel2  721  pm2.621  742  mtord  778  jaodan  792  pm2.63  795  pm2.74  802  dedlema  964  dedlemb  965  oplem1  970  opthpr  3759  trsucss  4408  ordsucim  4484  onsucelsucr  4492  0elnn  4603  xpsspw  4723  relop  4761  fununi  5266  poxp  6211  nntri1  6475  nnsseleq  6480  nnmordi  6495  nnaordex  6507  nnm00  6509  swoord2  6543  nneneq  6835  exmidonfinlem  7170  elni2  7276  prubl  7448  distrlem4prl  7546  distrlem4pru  7547  ltxrlt  7985  recexre  8497  remulext1  8518  mulext1  8531  un0addcl  9168  un0mulcl  9169  elnnz  9222  zleloe  9259  zindd  9330  uzsplit  10048  fzm1  10056  expcl2lemap  10488  expnegzap  10510  expaddzap  10520  expmulzap  10522  qsqeqor  10586  nn0opthd  10656  facdiv  10672  facwordi  10674  bcpasc  10700  recvguniq  10959  absexpzap  11044  maxabslemval  11172  xrmaxiflemval  11213  sumrbdclem  11340  summodc  11346  zsumdc  11347  prodrbdclem  11534  zproddc  11542  prodssdc  11552  fprodcl2lem  11568  fprodsplitsn  11596  ordvdsmul  11796  gcdaddm  11939  lcmdvds  12033  dvdsprime  12076  prmdvdsexpr  12104  prmfac1  12106  pythagtriplem2  12220  unct  12397  baspartn  12842  reopnap  13332  coseq0q4123  13549  lgsdir2lem2  13724  decidin  13832  bj-charfun  13842  bj-nntrans  13986  bj-nnelirr  13988  bj-findis  14014  exmid1stab  14033  triap  14061
  Copyright terms: Public domain W3C validator