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

Theorem jaod 670
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 669 . 2  |-  ( ( ps  \/  th )  ->  ( ph  ->  ch ) )
65com12 30 1  |-  ( ph  ->  ( ( ps  \/  th )  ->  ch )
)
Colors of variables: wff set class
Syntax hints:    -> wi 4    \/ wo 662
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 663
This theorem depends on definitions:  df-bi 115
This theorem is referenced by:  mpjaod  671  jaao  672  orel2  678  pm2.621  699  mtord  730  jaodan  744  pm2.63  747  pm2.74  754  dedlema  911  dedlemb  912  oplem1  917  opthpr  3572  trsucss  4186  ordsucim  4252  onsucelsucr  4260  0elnn  4366  xpsspw  4478  relop  4514  fununi  4998  poxp  5884  nntri1  6140  nnsseleq  6145  nnmordi  6155  nnaordex  6166  nnm00  6168  swoord2  6202  nneneq  6392  elni2  6566  prubl  6738  distrlem4prl  6836  distrlem4pru  6837  ltxrlt  7245  recexre  7745  remulext1  7766  mulext1  7779  un0addcl  8388  un0mulcl  8389  elnnz  8442  zleloe  8479  zindd  8546  uzsplit  9185  fzm1  9193  expcl2lemap  9585  expnegzap  9607  expaddzap  9617  expmulzap  9619  nn0opthd  9746  facdiv  9762  facwordi  9764  bcpasc  9790  recvguniq  10019  absexpzap  10104  maxabslemval  10232  isumrblem  10337  ordvdsmul  10381  gcdaddm  10519  lcmdvds  10605  dvdsprime  10648  prmdvdsexpr  10673  prmfac1  10675  decidin  10758  bj-nntrans  10904  bj-nnelirr  10906  bj-findis  10932
  Copyright terms: Public domain W3C validator