Theorem jaod 380

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 31	. . 3 |- ( ps -> ( ph -> ch ) )
3		jaod.2	. . . 4 |- ( ph -> ( th -> ch ) )
4	3	com12 31	. . 3 |- ( th -> ( ph -> ch ) )
5	2, 4	jaoi 379	. 2 |- ( ( ps \/ th ) -> ( ph -> ch ) )
6	5	com12 31	1 |- ( ph -> ( ( ps \/ th ) -> ch ) )

Syntax hints:   -> wi 4   \/ wo 368

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 185  df-or 370

This theorem is referenced by:  mpjaod  381  orel2  383  pm2.621  408  jaao  509  jaodan  783  pm2.63  786  ecase2d  938  ecase3d  941  dedlema  952  dedlemb  953  cad0  1453  psssstr  3592  opthpr  4189  sotric  4812  sotr2  4815  trsucss  4949  ordelinel  4962  xpsspw  5102  relop  5139  fununi  5640  fnprb  6110  fnprOLD  6111  soisoi  6205  ordunisuc2  6660  poxp  6893  soxp  6894  tfrlem11  7055  omordi  7213  om00  7222  odi  7226  omeulem2  7230  oewordi  7238  nnmordi  7278  omsmolem  7300  swoord2  7339  nneneq  7698  dffi3  7889  inf3lem6  8048  cantnfle  8088  cantnflem1  8106  cantnflem2  8107  cantnfleOLD  8118  cantnflem1OLD  8129  r1sdom  8190  r1ord3g  8195  rankxplim3  8297  carddom2  8356  wdomnumr  8443  alephordi  8453  alephdom  8460  cardaleph  8468  cdainf  8570  cfsuc  8635  cfsmolem  8648  sornom  8655  fin23lem25  8702  fin1a2lem11  8788  fin1a2s  8792  zorn2lem7  8880  ttukeylem5  8891  alephval2  8945  fpwwe2lem13  9018  gch2  9051  gchaclem  9054  prub  9370  sqgt0sr  9481  1re  9593  lelttr  9673  ltletr  9674  letr  9676  mul0or  10190  prodgt0  10388  mulge0b  10413  squeeze0  10449  sup2  10500  un0addcl  10830  un0mulcl  10831  nn0sub  10847  elnnz  10875  zindd  10965  rpneg  11253  xrlttri  11349  xrlelttr  11363  xrltletr  11364  xrletr  11365  qextlt  11406  qextle  11407  xmullem2  11461  xlemul1a  11484  xrsupexmnf  11500  xrinfmexpnf  11501  supxrun  11511  prunioo  11653  difreicc  11656  iccsplit  11657  uzsplit  11754  fzm1  11762  expcl2lem  12152  expeq0  12170  expnegz  12174  expaddz  12184  expmulz  12186  sqlecan  12248  facdiv  12339  facwordi  12341  bcpasc  12373  resqrex  13058  absexpz  13112  caubnd  13165  summo  13513  zsum  13514  rpnnen2  13831  ordvdsmul  13894  dvdsprime  14102  prmdvdsexpr  14129  prmfac1  14131  pythagtriplem2  14213  4sqlem11  14345  vdwlem6  14376  vdwlem9  14379  vdwlem13  14383  cshwshashlem3  14454  prmlem0  14463  xpscfv  14831  pleval2  15464  pltletr  15470  plelttr  15471  tsrlemax  15719  f1omvdco2  16342  psgnunilem2  16389  efgredlemc  16632  frgpuptinv  16658  lt6abl  16766  dmdprdsplit2lem  16962  drngmul0or  17285  lvecvs0or  17622  domneq0  17814  baspartn  19322  0top  19351  indistopon  19368  restntr  19549  cnindis  19659  cmpfi  19774  filcon  20250  ufprim  20276  ufildr  20298  alexsubALTlem2  20414  alexsubALTlem3  20415  alexsubALTlem4  20416  ovolicc2lem3  21796  rolle  22257  dvivthlem1  22275  coeaddlem  22511  dgrco  22537  plymul0or  22542  aalioulem3  22595  cxpge0  22929  cxpmul2z  22937  cxpcn3lem  22986  scvxcvx  23180  sqf11  23278  ppiublem1  23342  lgsdir2lem2  23464  lgsqrlem2  23482  lmieu  24015  frgraogt3nreg  24985  gxnn0neg  25130  gxnn0suc  25131  nvmul0or  25412  hvmul0or  25807  disjxpin  27312  subfacp1lem4  28493  untsucf  28948  zprod  29037  dfon2lem6  29188  dftrpred3g  29284  wfrlem14  29324  wfrlem15  29325  nodenselem4  29412  broutsideof2  29740  btwnoutside  29743  broutsideof3  29744  outsideoftr  29747  lineunray  29765  lineelsb2  29766  meran1  29844  ontgval  29864  ordcmp  29880  mblfinlem2  30020  ovoliunnfl  30024  itg2addnclem  30034  finminlem  30104  nn0prpw  30109  refssfne  30144  sdclem2  30203  fdc  30206  divrngidl  30393  fphpdo  30719  pellfundex  30790  jm2.19lem4  30902  jm2.26a  30910  lidldomn1  32427  uzlidlring  32435  bj-sngltag  34253  lkreqN  34597  cvrnbtwn4  34706  4atlem12  35038  elpaddn0  35226  paddasslem17  35262  paddidm  35267  pmapjoin  35278  llnexchb2  35295  dalawlem13  35309  dalawlem14  35310  dochkrshp4  36818  lcfl6  36929