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

Theorem jaod 672
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 671 . 2  |-  ( ( ps  \/  th )  ->  ( ph  ->  ch ) )
65com12 30 1  |-  ( ph  ->  ( ( ps  \/  th )  ->  ch )
)
Colors of variables: wff set class
Syntax hints:    -> wi 4    \/ wo 664
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-io 665
This theorem depends on definitions:  df-bi 115
This theorem is referenced by:  mpjaod  673  jaao  674  orel2  680  pm2.621  701  mtord  732  jaodan  746  pm2.63  749  pm2.74  756  dedlema  915  dedlemb  916  oplem1  921  opthpr  3611  trsucss  4241  ordsucim  4307  onsucelsucr  4315  0elnn  4422  xpsspw  4538  relop  4574  fununi  5068  poxp  5979  nntri1  6239  nnsseleq  6244  nnmordi  6255  nnaordex  6266  nnm00  6268  swoord2  6302  nneneq  6553  elni2  6852  prubl  7024  distrlem4prl  7122  distrlem4pru  7123  ltxrlt  7531  recexre  8031  remulext1  8052  mulext1  8065  un0addcl  8676  un0mulcl  8677  elnnz  8730  zleloe  8767  zindd  8834  uzsplit  9473  fzm1  9481  expcl2lemap  9932  expnegzap  9954  expaddzap  9964  expmulzap  9966  nn0opthd  10095  facdiv  10111  facwordi  10113  bcpasc  10139  recvguniq  10393  absexpzap  10478  maxabslemval  10606  isumrblem  10729  isummo  10737  zisum  10738  ordvdsmul  10919  gcdaddm  11057  lcmdvds  11143  dvdsprime  11186  prmdvdsexpr  11211  prmfac1  11213  decidin  11343  bj-nntrans  11492  bj-nnelirr  11494  bj-findis  11520
  Copyright terms: Public domain W3C validator