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  506  jaodan  776  pm2.63  779  ecase2d  924  ecase3d  927  dedlema  938  dedlemb  939  cad0  1445  psssstr  3450  opthpr  4038  sotric  4654  sotr2  4657  trsucss  4791  ordelinel  4804  xpsspw  4940  relop  4977  fununi  5472  fnprb  5923  fnprOLD  5924  soisoi  6006  ordunisuc2  6444  poxp  6673  soxp  6674  tfrlem11  6833  omordi  6993  om00  7002  odi  7006  omeulem2  7010  oewordi  7018  nnmordi  7058  omsmolem  7080  swoord2  7119  nneneq  7482  dffi3  7669  inf3lem6  7827  cantnfle  7867  cantnflem1  7885  cantnflem2  7886  cantnfleOLD  7897  cantnflem1OLD  7908  r1sdom  7969  r1ord3g  7974  rankxplim3  8076  carddom2  8135  wdomnumr  8222  alephordi  8232  alephdom  8239  cardaleph  8247  cdainf  8349  cfsuc  8414  cfsmolem  8427  sornom  8434  fin23lem25  8481  fin1a2lem11  8567  fin1a2s  8571  zorn2lem7  8659  ttukeylem5  8670  alephval2  8724  fpwwe2lem13  8796  gch2  8829  gchaclem  8832  prub  9150  sqgt0sr  9260  1re  9372  lelttr  9452  ltletr  9453  letr  9455  mul0or  9963  prodgt0  10161  mulge0b  10186  squeeze0  10222  sup2  10273  un0addcl  10600  un0mulcl  10601  nn0sub  10617  elnnz  10643  zindd  10730  rpneg  11007  xrlttri  11103  xrlelttr  11117  xrltletr  11118  xrletr  11119  qextlt  11160  qextle  11161  xmullem2  11215  xlemul1a  11238  xrsupexmnf  11254  xrinfmexpnf  11255  supxrun  11265  prunioo  11400  difreicc  11403  iccsplit  11404  uzsplit  11513  fzm1  11523  expcl2lem  11860  expeq0  11877  expnegz  11881  expaddz  11891  expmulz  11893  sqlecan  11955  facdiv  12046  facwordi  12048  bcpasc  12080  resqrex  12723  absexpz  12777  caubnd  12829  summo  13177  zsum  13178  rpnnen2  13490  ordvdsmul  13551  dvdsprime  13758  prmdvdsexpr  13784  prmfac1  13786  pythagtriplem2  13866  4sqlem11  13998  vdwlem6  14029  vdwlem9  14032  vdwlem13  14036  cshwshashlem3  14106  prmlem0  14115  xpscfv  14482  pleval2  15117  pltletr  15123  plelttr  15124  tsrlemax  15372  f1omvdco2  15933  psgnunilem2  15980  efgredlemc  16221  frgpuptinv  16247  lt6abl  16350  dmdprdsplit2lem  16517  drngmul0or  16776  lvecvs0or  17110  domneq0  17290  baspartn  18400  0top  18429  indistopon  18446  restntr  18627  cnindis  18737  cmpfi  18852  filcon  19297  ufprim  19323  ufildr  19345  alexsubALTlem2  19461  alexsubALTlem3  19462  alexsubALTlem4  19463  ovolicc2lem3  20843  rolle  21303  dvivthlem1  21321  coeaddlem  21600  dgrco  21626  plymul0or  21631  aalioulem3  21684  cxpge0  22012  cxpmul2z  22020  cxpcn3lem  22069  scvxcvx  22263  sqf11  22361  ppiublem1  22425  lgsdir2lem2  22547  lgsqrlem2  22565  gxnn0neg  23572  gxnn0suc  23573  nvmul0or  23854  hvmul0or  24249  disjxpin  25753  subfacp1lem4  26918  untsucf  27207  zprod  27296  dfon2lem6  27447  dftrpred3g  27543  wfrlem14  27583  wfrlem15  27584  nodenselem4  27671  broutsideof2  27999  btwnoutside  28002  broutsideof3  28003  outsideoftr  28006  lineunray  28024  lineelsb2  28025  meran1  28104  ontgval  28124  ordcmp  28140  mblfinlem2  28270  ovoliunnfl  28274  itg2addnclem  28284  finminlem  28354  nn0prpw  28359  refssfne  28407  sdclem2  28479  fdc  28482  divrngidl  28669  fphpdo  28998  pellfundex  29069  jm2.19lem4  29183  jm2.26a  29191  frgraogt3nreg  30556  bj-sngltag  32056  lkreqN  32385  cvrnbtwn4  32494  4atlem12  32826  elpaddn0  33014  paddasslem17  33050  paddidm  33055  pmapjoin  33066  llnexchb2  33083  dalawlem13  33097  dalawlem14  33098  dochkrshp4  34604  lcfl6  34715