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  1452  psssstr  3610  opthpr  4204  sotric  4826  sotr2  4829  trsucss  4963  ordelinel  4976  xpsspw  5114  relop  5151  fununi  5652  fnprb  6117  fnprOLD  6118  soisoi  6210  ordunisuc2  6657  poxp  6892  soxp  6893  tfrlem11  7054  omordi  7212  om00  7221  odi  7225  omeulem2  7229  oewordi  7237  nnmordi  7277  omsmolem  7299  swoord2  7338  nneneq  7697  dffi3  7887  inf3lem6  8046  cantnfle  8086  cantnflem1  8104  cantnflem2  8105  cantnfleOLD  8116  cantnflem1OLD  8127  r1sdom  8188  r1ord3g  8193  rankxplim3  8295  carddom2  8354  wdomnumr  8441  alephordi  8451  alephdom  8458  cardaleph  8466  cdainf  8568  cfsuc  8633  cfsmolem  8646  sornom  8653  fin23lem25  8700  fin1a2lem11  8786  fin1a2s  8790  zorn2lem7  8878  ttukeylem5  8889  alephval2  8943  fpwwe2lem13  9016  gch2  9049  gchaclem  9052  prub  9368  sqgt0sr  9479  1re  9591  lelttr  9671  ltletr  9672  letr  9674  mul0or  10185  prodgt0  10383  mulge0b  10408  squeeze0  10444  sup2  10495  un0addcl  10825  un0mulcl  10826  nn0sub  10842  elnnz  10870  zindd  10958  rpneg  11245  xrlttri  11341  xrlelttr  11355  xrltletr  11356  xrletr  11357  qextlt  11398  qextle  11399  xmullem2  11453  xlemul1a  11476  xrsupexmnf  11492  xrinfmexpnf  11493  supxrun  11503  prunioo  11645  difreicc  11648  iccsplit  11649  uzsplit  11746  fzm1  11754  expcl2lem  12142  expeq0  12160  expnegz  12164  expaddz  12174  expmulz  12176  sqlecan  12238  facdiv  12329  facwordi  12331  bcpasc  12363  resqrex  13043  absexpz  13097  caubnd  13150  summo  13498  zsum  13499  rpnnen2  13816  ordvdsmul  13877  dvdsprime  14085  prmdvdsexpr  14112  prmfac1  14114  pythagtriplem2  14196  4sqlem11  14328  vdwlem6  14359  vdwlem9  14362  vdwlem13  14366  cshwshashlem3  14436  prmlem0  14445  xpscfv  14813  pleval2  15448  pltletr  15454  plelttr  15455  tsrlemax  15703  f1omvdco2  16269  psgnunilem2  16316  efgredlemc  16559  frgpuptinv  16585  lt6abl  16688  dmdprdsplit2lem  16884  drngmul0or  17200  lvecvs0or  17537  domneq0  17717  baspartn  19222  0top  19251  indistopon  19268  restntr  19449  cnindis  19559  cmpfi  19674  filcon  20119  ufprim  20145  ufildr  20167  alexsubALTlem2  20283  alexsubALTlem3  20284  alexsubALTlem4  20285  ovolicc2lem3  21665  rolle  22126  dvivthlem1  22144  coeaddlem  22380  dgrco  22406  plymul0or  22411  aalioulem3  22464  cxpge0  22792  cxpmul2z  22800  cxpcn3lem  22849  scvxcvx  23043  sqf11  23141  ppiublem1  23205  lgsdir2lem2  23327  lgsqrlem2  23345  lmieu  23827  frgraogt3nreg  24797  gxnn0neg  24941  gxnn0suc  24942  nvmul0or  25223  hvmul0or  25618  disjxpin  27120  subfacp1lem4  28267  untsucf  28557  zprod  28646  dfon2lem6  28797  dftrpred3g  28893  wfrlem14  28933  wfrlem15  28934  nodenselem4  29021  broutsideof2  29349  btwnoutside  29352  broutsideof3  29353  outsideoftr  29356  lineunray  29374  lineelsb2  29375  meran1  29453  ontgval  29473  ordcmp  29489  mblfinlem2  29629  ovoliunnfl  29633  itg2addnclem  29643  finminlem  29713  nn0prpw  29718  refssfne  29766  sdclem2  29838  fdc  29841  divrngidl  30028  fphpdo  30355  pellfundex  30426  jm2.19lem4  30538  jm2.26a  30546  bj-sngltag  33622  lkreqN  33967  cvrnbtwn4  34076  4atlem12  34408  elpaddn0  34596  paddasslem17  34632  paddidm  34637  pmapjoin  34648  llnexchb2  34665  dalawlem13  34679  dalawlem14  34680  dochkrshp4  36186  lcfl6  36297