Theorem jaod 381

Description: Deduction disjoining the antecedents of two implications. (Contributed by NM, 18-Aug-1994.)

Hypotheses

Ref	Expression
jaod.1	|- ( ph -> ( ps -> ch ) )
jaod.2	|- ( ph -> ( th -> ch ) )

Assertion

Ref	Expression
jaod	|- ( ph -> ( ( ps \/ th ) -> ch ) )

Proof of Theorem jaod

Step	Hyp	Ref	Expression
1		jaod.1	. . . 4 |- ( ph -> ( ps -> ch ) )
2	1	com12 32	. . 3 |- ( ps -> ( ph -> ch ) )
3		jaod.2	. . . 4 |- ( ph -> ( th -> ch ) )
4	3	com12 32	. . 3 |- ( th -> ( ph -> ch ) )
5	2, 4	jaoi 380	. 2 |- ( ( ps \/ th ) -> ( ph -> ch ) )
6	5	com12 32	1 |- ( ph -> ( ( ps \/ th ) -> ch ) )

Syntax hints:   -> wi 4   \/ wo 369

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 188  df-or 371

This theorem is referenced by:  mpjaod  382  orel2  384  pm2.621  409  jaao  511  jaodan  792  pm2.63  795  ecase2d  948  ecase3d  951  dedlema  962  dedlemb  963  cad0  1515  psssstr  3577  opthpr  4181  sotric  4801  sotr2  4804  relop  5005  trsucss  5527  ordelinel  5540  fununi  5667  fnprb  6138  soisoi  6234  ordunisuc2  6685  poxp  6919  soxp  6920  wfrlem14  7057  wfrlem15  7058  tfrlem11  7114  omordi  7275  om00  7284  odi  7288  omeulem2  7292  oewordi  7300  nnmordi  7340  omsmolem  7362  swoord2  7401  nneneq  7761  dffi3  7951  inf3lem6  8138  cantnfle  8175  cantnflem1  8193  cantnflem2  8194  r1sdom  8244  r1ord3g  8249  rankxplim3  8351  carddom2  8410  wdomnumr  8493  alephordi  8503  alephdom  8510  cardaleph  8518  cdainf  8620  cfsuc  8685  cfsmolem  8698  sornom  8705  fin23lem25  8752  fin1a2lem11  8838  fin1a2s  8842  zorn2lem7  8930  ttukeylem5  8941  alephval2  8995  fpwwe2lem13  9066  gch2  9099  gchaclem  9102  prub  9418  sqgt0sr  9529  1re  9641  lelttr  9723  ltletr  9724  letr  9726  mul0or  10251  prodgt0  10449  mulge0b  10474  squeeze0  10509  sup2  10565  un0addcl  10903  un0mulcl  10904  nn0sub  10920  elnnz  10947  zindd  11036  rpneg  11332  xrlttri  11438  xrlelttr  11453  xrltletr  11454  xrletr  11455  qextlt  11496  qextle  11497  xmullem2  11551  xlemul1a  11574  xrsupexmnf  11590  xrinfmexpnf  11591  supxrun  11601  prunioo  11759  difreicc  11762  iccsplit  11763  uzsplit  11864  fzm1  11872  expcl2lem  12281  expeq0  12299  expnegz  12303  expaddz  12313  expmulz  12315  sqlecan  12378  facdiv  12469  facwordi  12471  bcpasc  12503  resqrex  13293  absexpz  13347  caubnd  13400  summo  13761  zsum  13762  zprod  13969  rpnnen2  14256  ordvdsmul  14319  dvdsprime  14608  prmdvdsexpr  14640  prmfac1  14642  pythagtriplem2  14730  4sqlem11  14862  vdwlem6  14899  vdwlem9  14902  vdwlem13  14906  cshwshashlem3  15031  prmlem0  15040  xpscfv  15419  pleval2  16162  pltletr  16168  plelttr  16169  tsrlemax  16417  f1omvdco2  17040  psgnunilem2  17087  efgredlemc  17330  frgpuptinv  17356  lt6abl  17464  dmdprdsplit2lem  17613  drngmul0or  17931  lvecvs0or  18266  domneq0  18456  baspartn  19900  0top  19930  indistopon  19947  restntr  20129  cnindis  20239  cmpfi  20354  filcon  20829  ufprim  20855  ufildr  20877  alexsubALTlem2  20994  alexsubALTlem3  20995  alexsubALTlem4  20996  ovolicc2lem3  22350  rolle  22819  dvivthlem1  22837  coeaddlem  23071  dgrco  23097  plymul0or  23102  aalioulem3  23155  cxpge0  23493  cxpmul2z  23501  cxpcn3lem  23552  scvxcvx  23776  sqf11  23929  ppiublem1  23993  lgsdir2lem2  24115  lgsqrlem2  24133  lmieu  24682  frgraogt3nreg  25693  gxnn0neg  25836  gxnn0suc  25837  nvmul0or  26118  hvmul0or  26513  disjxpin  28037  subfacp1lem4  29694  untsucf  30125  dfon2lem6  30221  dftrpred3g  30261  nodenselem4  30358  broutsideof2  30674  btwnoutside  30677  broutsideof3  30678  outsideoftr  30681  lineunray  30699  lineelsb2  30700  finminlem  30759  nn0prpw  30764  refssfne  30799  meran1  30856  ontgval  30876  ordcmp  30892  bj-sngltag  31326  topdifinfindis  31483  icoreclin  31494  poimirlem24  31668  poimirlem25  31669  poimirlem29  31673  poimirlem31  31675  mblfinlem2  31682  ovoliunnfl  31686  itg2addnclem  31697  sdclem2  31775  fdc  31778  divrngidl  31965  lkreqN  32445  cvrnbtwn4  32554  4atlem12  32886  elpaddn0  33074  paddasslem17  33110  paddidm  33115  pmapjoin  33126  llnexchb2  33143  dalawlem13  33157  dalawlem14  33158  dochkrshp4  34666  lcfl6  34777  fphpdo  35369  pellfundex  35440  jm2.19lem4  35553  jm2.26a  35561  relexpmulg  35941  relexp01min  35944  relexpxpmin  35948  relexpaddss  35949  gboge7  38254  bgoldbtbndlem3  38292  lidldomn1  38679  uzlidlring  38687