Theorem jaod 378

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 377	. 2 |- ( ( ps \/ th ) -> ( ph -> ch ) )
6	5	com12 31	1 |- ( ph -> ( ( ps \/ th ) -> ch ) )

Syntax hints:   -> wi 4   \/ wo 366

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 368

This theorem is referenced by:  mpjaod  379  orel2  381  pm2.621  406  jaao  507  jaodan  783  pm2.63  786  ecase2d  938  ecase3d  941  dedlema  952  dedlemb  953  cad0  1471  psssstr  3596  opthpr  4194  sotric  4815  sotr2  4818  trsucss  4952  ordelinel  4965  xpsspw  5104  relop  5142  fununi  5636  fnprb  6106  soisoi  6199  ordunisuc2  6652  poxp  6885  soxp  6886  tfrlem11  7049  omordi  7207  om00  7216  odi  7220  omeulem2  7224  oewordi  7232  nnmordi  7272  omsmolem  7294  swoord2  7333  nneneq  7693  dffi3  7883  inf3lem6  8041  cantnfle  8081  cantnflem1  8099  cantnflem2  8100  cantnfleOLD  8111  cantnflem1OLD  8122  r1sdom  8183  r1ord3g  8188  rankxplim3  8290  carddom2  8349  wdomnumr  8436  alephordi  8446  alephdom  8453  cardaleph  8461  cdainf  8563  cfsuc  8628  cfsmolem  8641  sornom  8648  fin23lem25  8695  fin1a2lem11  8781  fin1a2s  8785  zorn2lem7  8873  ttukeylem5  8884  alephval2  8938  fpwwe2lem13  9009  gch2  9042  gchaclem  9045  prub  9361  sqgt0sr  9472  1re  9584  lelttr  9664  ltletr  9665  letr  9667  mul0or  10185  prodgt0  10383  mulge0b  10408  squeeze0  10443  sup2  10494  un0addcl  10825  un0mulcl  10826  nn0sub  10842  elnnz  10870  zindd  10961  rpneg  11251  xrlttri  11348  xrlelttr  11362  xrltletr  11363  xrletr  11364  qextlt  11405  qextle  11406  xmullem2  11460  xlemul1a  11483  xrsupexmnf  11499  xrinfmexpnf  11500  supxrun  11510  prunioo  11652  difreicc  11655  iccsplit  11656  uzsplit  11754  fzm1  11762  expcl2lem  12163  expeq0  12181  expnegz  12185  expaddz  12195  expmulz  12197  sqlecan  12259  facdiv  12350  facwordi  12352  bcpasc  12384  resqrex  13169  absexpz  13223  caubnd  13276  summo  13624  zsum  13625  zprod  13829  rpnnen2  14046  ordvdsmul  14109  dvdsprime  14317  prmdvdsexpr  14344  prmfac1  14346  pythagtriplem2  14428  4sqlem11  14560  vdwlem6  14591  vdwlem9  14594  vdwlem13  14598  cshwshashlem3  14669  prmlem0  14678  xpscfv  15054  pleval2  15797  pltletr  15803  plelttr  15804  tsrlemax  16052  f1omvdco2  16675  psgnunilem2  16722  efgredlemc  16965  frgpuptinv  16991  lt6abl  17099  dmdprdsplit2lem  17292  drngmul0or  17615  lvecvs0or  17952  domneq0  18144  baspartn  19625  0top  19655  indistopon  19672  restntr  19853  cnindis  19963  cmpfi  20078  filcon  20553  ufprim  20579  ufildr  20601  alexsubALTlem2  20717  alexsubALTlem3  20718  alexsubALTlem4  20719  ovolicc2lem3  22099  rolle  22560  dvivthlem1  22578  coeaddlem  22815  dgrco  22841  plymul0or  22846  aalioulem3  22899  cxpge0  23235  cxpmul2z  23243  cxpcn3lem  23292  scvxcvx  23516  sqf11  23614  ppiublem1  23678  lgsdir2lem2  23800  lgsqrlem2  23818  lmieu  24354  frgraogt3nreg  25325  gxnn0neg  25466  gxnn0suc  25467  nvmul0or  25748  hvmul0or  26143  disjxpin  27661  subfacp1lem4  28894  untsucf  29326  dfon2lem6  29463  dftrpred3g  29559  wfrlem14  29599  wfrlem15  29600  nodenselem4  29687  broutsideof2  30003  btwnoutside  30006  broutsideof3  30007  outsideoftr  30010  lineunray  30028  lineelsb2  30029  meran1  30107  ontgval  30127  ordcmp  30143  mblfinlem2  30295  ovoliunnfl  30299  itg2addnclem  30309  finminlem  30379  nn0prpw  30384  refssfne  30419  sdclem2  30478  fdc  30481  divrngidl  30668  fphpdo  30993  pellfundex  31064  jm2.19lem4  31176  jm2.26a  31184  lidldomn1  33000  uzlidlring  33008  bj-sngltag  34961  lkreqN  35311  cvrnbtwn4  35420  4atlem12  35752  elpaddn0  35940  paddasslem17  35976  paddidm  35981  pmapjoin  35992  llnexchb2  36009  dalawlem13  36023  dalawlem14  36024  dochkrshp4  37532  lcfl6  37643  relexpaddss  38226  relexp01min  38240  relexpxpmin  38247  relexpmulg  38249