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 )

This proof depends on syntax axioms:   -> wi 4   \/ wo 720

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 721

This proof depends on definitions:  df-bi 117

This theorem is used 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  3652  ifsbdc  3653  ifiddc  3676  eqifdc  3677  ifnotdc  3679  ifandc  3681  ifordc  3682  elpr2  3731  rabsnifsb  3777  sssnr  3878  ssprr  3881  sstpr  3882  preq12b  3895  elpr2elpr  3901  exmidn0m  4338  copsexg  4384  sotritric  4469  regexmidlem1  4680  nn0eln0  4767  xpeq0r  5210  funtpg  5432  acexmidlemcase  6080  acexmidlem2  6082  el2oss1o  6716  nnm00  6803  djuss  7411  eldju2ndl  7413  eldju2ndr  7414  updjud  7423  nnnninf2  7468  sspw1or2  7545  exmidonfinlem  7546  exmidfodomrlemim  7554  exmidaclem  7565  renfdisj  8386  sup3exmid  9290  nn0ge0  9593  elnnnn0b  9612  xnn0xr  9640  xnn0nemnf  9646  elnn0z  9662  nn0n0n1ge2b  9730  nn0le2is012  9733  nn0ind-raph  9768  uzin  9965  elnn1uz2  10017  indstr2  10019  nn0ledivnn  10179  xrnemnf  10190  xrnepnf  10191  mnfltxr  10199  nn0pnfge0  10204  xnn0lenn0nn0  10278  xnn0xadd0  10280  elfzonlteqm1  10639  xqltnle  10713  flapcl  10722  flaplelt  10724  flapge  10731  fldiv4p1lem1div2  10754  fldiv4lem1div2  10756  flqeqceilz  10769  modfzo0difsn  10846  m1expcl2  11012  m1expeven  11037  resq01  11109  zzlesq  11160  facp1  11183  faclbnd3  11196  bcn1  11211  hashinfuni  11231  hashfzp1  11280  swrdnd  11446  pfxccatin12  11520  swrdccat  11522  pfxccat3a  11525  sq01  11675  isumz  12174  arisum  12283  arisum2  12284  ntrivcvgap  12333  prod1dc  12371  fprodfac  12400  mulsucdiv2z  12670  nn0o1gt2  12690  nno  12691  nn0o  12692  dfgcd2  12809  mulgcd  12811  gcdmultiplez  12816  dvdssq  12826  cncongr2  12900  prm2orodd  12922  dfphi2  13020  nnnn0modprm0  13056  prm23lt5  13064  pcmptcl  13143  oddprmdvds  13155  4sqlem19  13210  mulgnn0gzsum  13982  recnprss  15840  dvexp2  15865  dvmptid  15869  coseq0negpitopi  15990  logfac  16051  lgslem4  16244  gausslemma2dlem0i  16298  lgsquadlem2  16319  2lgslem3  16342  2lgs  16345  2lgsoddprmlem3  16352  upgrm  16463  upgrfi  16465  upgrex  16466  upgruhgr  16474  uspgrushgr  16543  uhgr2edg  16569  usgredg4  16578  upgriswlkdc  16723  umgrclwwlkge2  16765  eupth2lem3lem4fi  16836  konigsberg  16856  bj-dcstab  16906  bj-nn0suc  17112  bj-inf2vnlem2  17119  bj-nn0sucALT  17126  012of  17145  2o01f  17146