Theorem jaoi 728

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 727	. 2 |- ( ( ( ph -> ps ) /\ ( ch -> ps ) ) -> ( ( ph \/ ch ) -> ps ) )
4	1, 2, 3	mp2an 430	1 |- ( ( ph \/ ch ) -> ps )

Syntax hints:   -> wi 4   \/ wo 720

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 721

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  jaod  729  jaoa  732  imorr  733  pm2.53  734  pm1.4  739  imorri  761  ioran  764  pm3.14  765  pm1.2  768  orim12i  771  pm1.5  777  pm2.41  788  pm2.42  789  pm2.4  790  pm4.44  791  pm4.78i  794  jaoian  807  jao1i  808  pm2.64  813  pm2.76  820  pm2.82  824  pm3.2ni  825  andi  830  dcim  853  condcOLD  866  pm2.61ddc  873  pm5.18dc  895  pm2.85dc  917  peircedc  926  dcor  948  pm4.42r  984  oplem1  988  ifp2  993  ifpiddc  1004  1fpid3  1007  xoranor  1426  biassdc  1444  anxordi  1449  19.33  1537  hbequid  1566  hbor  1599  19.30dc  1680  19.43  1681  19.32r  1732  hbae  1770  equvini  1811  equveli  1812  exdistrfor  1853  dveeq2  1868  dveeq2or  1869  sbequi  1892  nfsbxy  2002  nfsbxyt  2003  sbcomxyyz  2032  dvelimALT  2070  dvelimfv  2071  dvelimor  2078  modc  2130  mooran1  2159  moexexdc  2171  rgen2a  2604  r19.32r  2697  eueq2dc  2999  eueq3dc  3000  sbcor  3096  elun  3370  ssun  3408  inss  3461  undif3ss  3492  elif  3649  ifsbdc  3650  ifiddc  3673  eqifdc  3674  ifnotdc  3676  ifandc  3678  ifordc  3679  elpr2  3727  rabsnifsb  3773  sssnr  3873  ssprr  3876  sstpr  3877  preq12b  3890  elpr2elpr  3896  exmidn0m  4333  copsexg  4379  sotritric  4464  regexmidlem1  4675  nn0eln0  4762  xpeq0r  5205  funtpg  5427  acexmidlemcase  6070  acexmidlem2  6072  el2oss1o  6706  nnm00  6793  djuss  7400  eldju2ndl  7402  eldju2ndr  7403  updjud  7412  nnnninf2  7457  sspw1or2  7534  exmidonfinlem  7535  exmidfodomrlemim  7543  exmidaclem  7554  renfdisj  8375  sup3exmid  9277  nn0ge0  9567  elnnnn0b  9586  xnn0xr  9614  xnn0nemnf  9620  elnn0z  9636  nn0n0n1ge2b  9704  nn0le2is012  9707  nn0ind-raph  9742  uzin  9934  elnn1uz2  9986  indstr2  9988  nn0ledivnn  10147  xrnemnf  10158  xrnepnf  10159  mnfltxr  10167  nn0pnfge0  10172  xnn0lenn0nn0  10246  xnn0xadd0  10248  elfzonlteqm1  10606  xqltnle  10680  fldiv4p1lem1div2  10718  fldiv4lem1div2  10720  flqeqceilz  10733  modfzo0difsn  10810  m1expcl2  10976  m1expeven  11001  resq01  11073  zzlesq  11124  facp1  11146  faclbnd3  11159  bcn1  11174  hashinfuni  11194  hashfzp1  11243  swrdnd  11409  pfxccatin12  11483  swrdccat  11485  pfxccat3a  11488  sq01  11638  isumz  12134  arisum  12243  arisum2  12244  ntrivcvgap  12293  prod1dc  12331  fprodfac  12360  mulsucdiv2z  12630  nn0o1gt2  12650  nno  12651  nn0o  12652  dfgcd2  12769  mulgcd  12771  gcdmultiplez  12776  dvdssq  12786  cncongr2  12860  prm2orodd  12882  dfphi2  12976  nnnn0modprm0  13012  prm23lt5  13020  pcmptcl  13099  oddprmdvds  13111  4sqlem19  13166  mulgnn0gzsum  13908  recnprss  15711  dvexp2  15736  dvmptid  15740  coseq0negpitopi  15860  logfac  15918  lgslem4  16036  gausslemma2dlem0i  16090  lgsquadlem2  16111  2lgslem3  16134  2lgs  16137  2lgsoddprmlem3  16144  upgrm  16255  upgrfi  16257  upgrex  16258  upgruhgr  16266  uspgrushgr  16335  uhgr2edg  16361  usgredg4  16370  upgriswlkdc  16515  umgrclwwlkge2  16557  eupth2lem3lem4fi  16628  konigsberg  16648  bj-dcstab  16698  bj-nn0suc  16904  bj-inf2vnlem2  16911  bj-nn0sucALT  16918  012of  16937  2o01f  16938