Theorem jaoi 368

Description: Inference disjoining the antecedents of two implications.

Hypotheses

Ref	Expression
jaoi.1	|- (ph -> ps)
jaoi.2	|- (ch -> ps)

Assertion

Ref	Expression
jaoi	|- ((ph \/ ch) -> ps)

Proof of Theorem jaoi

Step	Hyp	Ref	Expression
1		jaoi.1	. 2 |- (ph -> ps)
2		jaoi.2	. 2 |- (ch -> ps)
3		jao 367	. 2 |- ((ph -> ps) -> ((ch -> ps) -> ((ph \/ ch) -> ps)))
4	1, 2, 3	mp2 54	1 |- ((ph \/ ch) -> ps)

Syntax hints:   -> wi 3   \/ wo 239

This theorem is referenced by:  pm2.41 369  pm2.42 370  pm2.4 371  pm4.44 372  pm5.63 373  jaoian 470  jaoa 473  pm2.64 475  pm2.75 634  pm2.8 636  pm2.82 638  pm5.18OLD 723  orbidi 815  ccase 829  consensus 844  consensusOLD 845  prlem1OLD 849  prlem2 850  dn1 855  dn1OLD 856  19.33 1443  19.33b 1444  19.33bOLD 1445  equviniOLD 1532  dfsb2 1595  mooran1 1822  mooran1OLD 1823  2eu3 1855  eueq3 2430  sspss 2707  ssnpssOLD 2713  sspsstr 2715  elun 2741  ssun 2782  undif3 2854  ifbi 2995  elpr2 3062  pwpw0 3134  sssn 3142  sspr 3144  snsssn 3148  preq12b 3154  pwsnALT 3173  unissint 3241  iununiOLD 3332  zfpair 3522  opth1 3531  pwundif 3579  ordssun 3769  ordequn 3770  onun2i 3785  unizlim 3786  eufromeq6 3833  ordeleqon 3866  ordunisuc 3911  ordunisucOLD 3912  orduninsuc 3925  onzslOLD 3929  tfinds 3942  tfindsOLD 3943  limomss 3956  limom 3967  onxpdisj 4068  onxpdisjOLD 4069  erref 5333  domnsym 5526  domsdomtr 5539  rankun 5802  brdom3 5963  iscard3 6036  indpi 6186  prlem934 6291  suppsr2 6375  ltlen 6692  renfdisj 6712  mnfltxr 6720  addgegt0iOLD 6780  msqgt0i 6794  mul0ori 6882  prodgt0i 6997  posexi 7091  elnn0z 7356  nn0sub 7370  elnn0nn 7380  nn0ind-raph 7426  zindd 7427  exple1 7852  sumsqne0i 7879  sq01 7897  discrlem 7909  nn0opthi 7916  sqrthi 7949  sqrcli 7950  sqrge0i 7952  leabsi 8124  nn0abscl 8131  facp1 8188  faclbnd3 8199  faclbnd4lem1 8200  faclbnd4lem3 8202  bcpasci 8221  binomi 8332  abspef01tlubi 8660  efgt0i 8669  infxpidmlem4 8824  infxpidmlem7 8827  sn0top 8917  metxptval 9107  dscmet 9196  efifolem2 10077  dif1card 10177  usinuniop 10341  shunssi 10970  cvmdi 11896  bnj962 12856  bnj1406 13116  bnj1431 13126  elnn00nn 13602  divalglem1 13697  divalglem6 13701  gcdaddmlem 13734  nepss 13820  dfon2lem7 13855  ordsucuniel 13863  trcllem1 13933  soxp 13950  axfelem12 14042  altopth1sn 14090  dissym1 14245  facrm 14290  nxtor 14312  neiopne 14354  repfuntw 14502  repcpwti 14503  cbcpcp 14504  tolat 14631  dfdir2 14639  mapudiscn 14872  top2usne 14898  subtopsin2 14907  clindistop 14962  cntrsetlem 14999  fldleqt 15023  vtarsuelt 15272  inttarcar 15278  alexsublem2 15438  alexsublem3 15439  filssufillem 15570  filnetlem1 15640  prfOLD 15680  difxp 15690  fimax 15746  piececn 15894  prtlem1 16230  19.33-2 16335  en3lpVD 16669  undif3VD 16706  stb2xpl 16742  elpadd0 17270

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7

This theorem depends on definitions:  df-bi 164  df-or 241  df-an 242

Copyright terms: Public domain