Theorem jaoi 348

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 347	. 2 |- ((ph -> ps) -> ((ch -> ps) -> ((ph \/ ch) -> ps)))
4	1, 2, 3	mp2 43	1 |- ((ph \/ ch) -> ps)

Syntax hints:   -> wi 3   \/ wo 229

This theorem is referenced by:  pm2.41 349  pm2.42 350  pm2.4 351  pm4.44 352  pm5.63 353  jaoian 434  jaoa 437  pm2.64 439  pm2.75 585  pm2.8 587  pm2.82 589  pm5.18 671  orbidi 755  ccase 767  consensus 779  prlem1 782  19.33 1132  19.33b 1133  equvini 1210  dfsb2 1267  mooran1 1467  2eu3 1494  eueq3 1966  sspss 2196  ssnpss 2200  sspsstr 2202  elun 2224  ssun 2257  ifbi 2423  elpr2 2477  pwpw0 2523  sssn 2527  sspr 2529  snsssn 2532  preq12b 2537  pwsnALT 2555  iununi 2671  zfpair 2833  opth1 2842  pwundif 2884  ordeleqon 3047  ordssun 3136  ordequn 3137  ordunisuc 3146  onun2i 3167  unizlim 3170  orduninsuc 3171  onzsl 3174  limomss 3194  limom 3203  tfinds 3218  onxpdisj 3298  erref 4333  domnsym 4526  domsdomtr 4539  rankun 4753  brdom3 4863  iscard3 4953  indpi 5099  prlem934 5204  suppsr2 5288  ltlen 5587  mnfltxr 5610  addgegt0i 5665  msqgt0i 5678  mul0ori 5759  prodgt0i 5877  posexi 5968  elnn0z 6229  nn0sub 6243  elnn0nn 6253  nn0ind-raph 6299  exple1 6696  sumsqne0i 6723  sq01 6740  discrlem 6749  sqrthi 6789  sqrcli 6790  sqrge0i 6792  leabsi 6962  nn0abscl 6969  facp1 7026  faclbnd3 7037  faclbnd4lem1 7038  faclbnd4lem3 7040  bcpasci 7059  binomi 7162  abspef01tlubi 7486  efgt0i 7495  infxpidmlem4 7647  infxpidmlem7 7650  sn0top 7734  metxptval 7915  dscmet 8003  efifolem2 8806  shunssi 9420  cvmdi 10335  neiopne 10554  mapudiscn 10606  top2usne 10643  usinuniop 10703

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 154  df-or 231  df-an 232

Copyright terms: Public domain