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

Theorem jaod 689
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 688 . 2  |-  ( ( ps  \/  th )  ->  ( ph  ->  ch ) )
65com12 30 1  |-  ( ph  ->  ( ( ps  \/  th )  ->  ch )
)
Colors of variables: wff set class
Syntax hints:    -> wi 4    \/ wo 680
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 681
This theorem depends on definitions:  df-bi 116
This theorem is referenced by:  mpjaod  690  jaao  691  orel2  698  pm2.621  719  mtord  755  jaodan  769  pm2.63  772  pm2.74  779  dedlema  936  dedlemb  937  oplem1  942  opthpr  3667  trsucss  4313  ordsucim  4384  onsucelsucr  4392  0elnn  4500  xpsspw  4619  relop  4657  fununi  5159  poxp  6095  nntri1  6358  nnsseleq  6363  nnmordi  6378  nnaordex  6389  nnm00  6391  swoord2  6425  nneneq  6717  elni2  7086  prubl  7258  distrlem4prl  7356  distrlem4pru  7357  ltxrlt  7794  recexre  8303  remulext1  8324  mulext1  8337  un0addcl  8961  un0mulcl  8962  elnnz  9015  zleloe  9052  zindd  9120  uzsplit  9812  fzm1  9820  expcl2lemap  10245  expnegzap  10267  expaddzap  10277  expmulzap  10279  nn0opthd  10408  facdiv  10424  facwordi  10426  bcpasc  10452  recvguniq  10707  absexpzap  10792  maxabslemval  10920  xrmaxiflemval  10959  sumrbdclem  11085  summodc  11092  zsumdc  11093  ordvdsmul  11430  gcdaddm  11568  lcmdvds  11656  dvdsprime  11699  prmdvdsexpr  11724  prmfac1  11726  unct  11849  baspartn  12112  reopnap  12602  decidin  12815  bj-nntrans  12960  bj-nnelirr  12962  bj-findis  12988  exmid1stab  13006  triap  13035
  Copyright terms: Public domain W3C validator