Theorem jaoi 668

Description: Inference disjoining the antecedents of two implications. (Contributed by NM, 5-Apr-1994.) (Revised by NM, 31-Jan-2015.)

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		pm3.44 667	. 2 |- ( ( ( ph -> ps ) /\ ( ch -> ps ) ) -> ( ( ph \/ ch ) -> ps ) )
4	1, 2, 3	mp2an 416	1 |- ( ( ph \/ ch ) -> ps )

Syntax hints:   -> wi 4   \/ wo 661

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 662

This theorem depends on definitions:  df-bi 115

This theorem is referenced by:  jaod  669  jaoa  672  pm2.53  673  pm1.4  678  imorri  700  ioran  701  pm3.14  702  pm1.2  705  orim12i  708  pm1.5  714  pm2.41  725  pm2.42  726  pm2.4  727  pm4.44  728  jaoian  741  jao1i  742  pm2.64  747  pm2.76  754  pm2.82  758  pm3.2ni  759  andi  764  condc  782  pm2.61ddc  791  pm5.18dc  810  dcim  817  imorr  830  pm4.78i  841  pm2.85dc  844  peircedc  853  dcan  875  dcor  876  pm4.42r  912  oplem1  916  xoranor  1308  biassdc  1326  anxordi  1331  19.33  1413  hbequid  1446  hbor  1478  19.30dc  1558  19.43  1559  19.32r  1610  hbae  1646  equvini  1681  equveli  1682  exdistrfor  1721  dveeq2  1736  dveeq2or  1737  sbequi  1760  nfsbxy  1859  nfsbxyt  1860  sbcomxyyz  1887  dvelimALT  1927  dvelimfv  1928  dvelimor  1935  modc  1984  mooran1  2013  moexexdc  2025  rgen2a  2417  r19.32r  2501  eueq2dc  2765  eueq3dc  2766  sbcor  2858  elun  3113  ssun  3151  inss  3195  undif3ss  3225  ifsbdc  3363  elpr2  3420  sssnr  3545  ssprr  3548  sstpr  3549  preq12b  3562  copsexg  3999  sotritric  4079  regexmidlem1  4276  nn0eln0  4359  xpeq0r  4766  funtpg  4970  acexmidlemcase  5527  acexmidlem2  5529  nnm00  6125  renfdisj  7172  nn0ge0  8313  elnnnn0b  8332  elnn0z  8364  nn0n0n1ge2b  8427  nn0ind-raph  8464  uzin  8651  elnn1uz2  8694  indstr2  8696  nn0ledivnn  8838  xrnemnf  8853  xrnepnf  8854  mnfltxr  8861  nn0pnfge0  8866  elfzonlteqm1  9219  fldiv4p1lem1div2  9307  flqeqceilz  9320  modfzo0difsn  9397  m1expcl2  9498  m1expeven  9523  facp1  9657  faclbnd3  9670  bcn1  9685  mulsucdiv2z  10285  nn0o1gt2  10305  nno  10306  nn0o  10307  dfgcd2  10403  mulgcd  10405  gcdmultiplez  10410  dvdssq  10420  cncongr2  10486  prm2orodd  10508  bj-nn0suc  10759  bj-inf2vnlem2  10766  bj-nn0sucALT  10773