Theorem jaoi 623

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

Syntax hints:   -> wi 4   \/ wo 616

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-io 617

This theorem depends on definitions:  df-bi 110

This theorem is referenced by:  jaod  624  jaoa  627  pm2.53  628  pm1.4  633  imorri  655  ioran  656  pm3.14  657  pm1.2  660  orim12i  663  pm1.5  669  pm2.41  680  pm2.42  681  pm2.4  682  pm4.44  683  jaoian  696  pm2.64  701  pm2.76  708  pm2.82  712  pm3.2ni  713  andi  719  condc  740  pm2.61ddc  751  pm5.18dc  770  dcim  777  imorr  790  pm4.78i  801  pm2.85dc  804  peircedc  813  dcan  830  dcor  831  pm4.42r  866  oplem1  870  xoranor  1253  biassdc  1269  anxordi  1274  19.33  1353  hbequid  1387  hbor  1420  19.30dc  1500  19.43  1501  19.32r  1552  hbae  1588  equvini  1623  equveli  1624  exdistrfor  1663  dveeq2  1678  dveeq2or  1679  sbequi  1702  nfsbxy  1800  nfsbxyt  1801  sbcomxyyz  1828  dvelimALT  1868  dvelimfv  1869  dvelimor  1876  modc  1925  mooran1  1954  moexexdc  1966  rgen2a  2353  r19.32r  2435  eueq2dc  2691  eueq3dc  2692  sbcor  2784  sspssr  3020  elun  3061  ssun  3099  inss  3143  undif3ss  3175  elpr2  3369  sssnr  3498  ssprr  3501  sstpr  3502  preq12b  3515  copsexg  3955  sotritric  4035  regexmidlem1  4202  nn0eln0  4268  xpeq0r  4673  funtpg  4876  acexmidlemcase  5431  acexmidlem2  5433  nnm00  6013  renfdisj  6680  bj-nn0suc  7182  bj-inf2vnlem2  7189  bj-nn0sucALT  7196