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  1513  psssstr  3507  opthpr  4114  sotric  4736  sotr2  4739  relop  4940  trsucss  5463  ordelinel  5476  fununi  5603  fnprb  6075  soisoi  6171  ordunisuc2  6622  poxp  6856  soxp  6857  wfrlem14  6997  wfrlem15  6998  tfrlem11  7054  omordi  7215  om00  7224  odi  7228  omeulem2  7232  oewordi  7240  nnmordi  7280  omsmolem  7302  swoord2  7341  nneneq  7701  dffi3  7891  inf3lem6  8084  cantnfle  8121  cantnflem1  8139  cantnflem2  8140  r1sdom  8190  r1ord3g  8195  rankxplim3  8297  carddom2  8356  wdomnumr  8439  alephordi  8449  alephdom  8456  cardaleph  8464  cdainf  8566  cfsuc  8631  cfsmolem  8644  sornom  8651  fin23lem25  8698  fin1a2lem11  8784  fin1a2s  8788  zorn2lem7  8876  ttukeylem5  8887  alephval2  8941  fpwwe2lem13  9011  gch2  9044  gchaclem  9047  prub  9363  sqgt0sr  9474  1re  9586  lelttr  9668  ltletr  9669  letr  9671  mul0or  10196  prodgt0  10394  mulge0b  10419  squeeze0  10453  sup2  10509  un0addcl  10847  un0mulcl  10848  nn0sub  10864  elnnz  10891  zindd  10980  rpneg  11276  xrlttri  11382  xrlelttr  11397  xrltletr  11398  xrletr  11399  qextlt  11440  qextle  11441  xmullem2  11495  xlemul1a  11518  xrsupexmnf  11534  xrinfmexpnf  11535  supxrun  11545  prunioo  11705  difreicc  11708  iccsplit  11709  uzsplit  11810  fzm1  11818  expcl2lem  12227  expeq0  12245  expnegz  12249  expaddz  12259  expmulz  12261  sqlecan  12324  facdiv  12415  facwordi  12417  bcpasc  12449  resqrex  13251  absexpz  13305  caubnd  13358  summo  13719  zsum  13720  zprod  13927  rpnnen2  14214  ordvdsmul  14277  dvdsprime  14573  prmdvdsexpr  14605  prmfac1  14607  pythagtriplem2  14703  4sqlem11  14835  vdwlem6  14872  vdwlem9  14875  vdwlem13  14879  cshwshashlem3  15004  prmlem0  15013  xpscfv  15404  pleval2  16147  pltletr  16153  plelttr  16154  tsrlemax  16402  f1omvdco2  17025  psgnunilem2  17072  efgredlemc  17331  frgpuptinv  17357  lt6abl  17465  dmdprdsplit2lem  17614  drngmul0or  17932  lvecvs0or  18267  domneq0  18457  baspartn  19904  0top  19934  indistopon  19951  restntr  20133  cnindis  20243  cmpfi  20358  filcon  20833  ufprim  20859  ufildr  20881  alexsubALTlem2  20998  alexsubALTlem3  20999  alexsubALTlem4  21000  ovolicc2lem3  22407  rolle  22877  dvivthlem1  22895  coeaddlem  23138  dgrco  23164  plymul0or  23169  aalioulem3  23225  cxpge0  23563  cxpmul2z  23571  cxpcn3lem  23622  scvxcvx  23846  sqf11  24001  ppiublem1  24065  lgsdir2lem2  24187  lgsqrlem2  24205  lmieu  24761  frgraogt3nreg  25783  gxnn0neg  25926  gxnn0suc  25927  nvmul0or  26208  hvmul0or  26613  disjxpin  28137  subfacp1lem4  29851  untsucf  30282  dfon2lem6  30378  dftrpred3g  30418  nodenselem4  30515  broutsideof2  30831  btwnoutside  30834  broutsideof3  30835  outsideoftr  30838  lineunray  30856  lineelsb2  30857  finminlem  30916  nn0prpw  30921  refssfne  30956  meran1  31013  ontgval  31033  ordcmp  31049  bj-sngltag  31482  topdifinfindis  31650  icoreclin  31661  finxpsuclem  31690  poimirlem24  31865  poimirlem25  31866  poimirlem29  31870  poimirlem31  31872  mblfinlem2  31879  ovoliunnfl  31883  itg2addnclem  31894  sdclem2  31972  fdc  31975  divrngidl  32162  lkreqN  32642  cvrnbtwn4  32751  4atlem12  33083  elpaddn0  33271  paddasslem17  33307  paddidm  33312  pmapjoin  33323  llnexchb2  33340  dalawlem13  33354  dalawlem14  33355  dochkrshp4  34863  lcfl6  34974  fphpdo  35566  pellfundex  35641  jm2.19lem4  35754  jm2.26a  35762  relexpmulg  36209  relexp01min  36212  relexpxpmin  36216  relexpaddss  36217  gboge7  38671  bgoldbtbndlem3  38709  upgredg  38984  lidldomn1  39506  uzlidlring  39514