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  931  ecase3d  934  dedlema  945  dedlemb  946  cad0  1442  psssstr  3467  opthpr  4055  sotric  4672  sotr2  4675  trsucss  4809  ordelinel  4822  xpsspw  4958  relop  4995  fununi  5489  fnprb  5941  fnprOLD  5942  soisoi  6024  ordunisuc2  6460  poxp  6689  soxp  6690  tfrlem11  6852  omordi  7010  om00  7019  odi  7023  omeulem2  7027  oewordi  7035  nnmordi  7075  omsmolem  7097  swoord2  7136  nneneq  7499  dffi3  7686  inf3lem6  7844  cantnfle  7884  cantnflem1  7902  cantnflem2  7903  cantnfleOLD  7914  cantnflem1OLD  7925  r1sdom  7986  r1ord3g  7991  rankxplim3  8093  carddom2  8152  wdomnumr  8239  alephordi  8249  alephdom  8256  cardaleph  8264  cdainf  8366  cfsuc  8431  cfsmolem  8444  sornom  8451  fin23lem25  8498  fin1a2lem11  8584  fin1a2s  8588  zorn2lem7  8676  ttukeylem5  8687  alephval2  8741  fpwwe2lem13  8814  gch2  8847  gchaclem  8850  prub  9168  sqgt0sr  9278  1re  9390  lelttr  9470  ltletr  9471  letr  9473  mul0or  9981  prodgt0  10179  mulge0b  10204  squeeze0  10240  sup2  10291  un0addcl  10618  un0mulcl  10619  nn0sub  10635  elnnz  10661  zindd  10748  rpneg  11025  xrlttri  11121  xrlelttr  11135  xrltletr  11136  xrletr  11137  qextlt  11178  qextle  11179  xmullem2  11233  xlemul1a  11256  xrsupexmnf  11272  xrinfmexpnf  11273  supxrun  11283  prunioo  11419  difreicc  11422  iccsplit  11423  uzsplit  11535  fzm1  11545  expcl2lem  11882  expeq0  11899  expnegz  11903  expaddz  11913  expmulz  11915  sqlecan  11977  facdiv  12068  facwordi  12070  bcpasc  12102  resqrex  12745  absexpz  12799  caubnd  12851  summo  13199  zsum  13200  rpnnen2  13513  ordvdsmul  13574  dvdsprime  13781  prmdvdsexpr  13807  prmfac1  13809  pythagtriplem2  13889  4sqlem11  14021  vdwlem6  14052  vdwlem9  14055  vdwlem13  14059  cshwshashlem3  14129  prmlem0  14138  xpscfv  14505  pleval2  15140  pltletr  15146  plelttr  15147  tsrlemax  15395  f1omvdco2  15959  psgnunilem2  16006  efgredlemc  16247  frgpuptinv  16273  lt6abl  16376  dmdprdsplit2lem  16549  drngmul0or  16858  lvecvs0or  17194  domneq0  17374  baspartn  18564  0top  18593  indistopon  18610  restntr  18791  cnindis  18901  cmpfi  19016  filcon  19461  ufprim  19487  ufildr  19509  alexsubALTlem2  19625  alexsubALTlem3  19626  alexsubALTlem4  19627  ovolicc2lem3  21007  rolle  21467  dvivthlem1  21485  coeaddlem  21721  dgrco  21747  plymul0or  21752  aalioulem3  21805  cxpge0  22133  cxpmul2z  22141  cxpcn3lem  22190  scvxcvx  22384  sqf11  22482  ppiublem1  22546  lgsdir2lem2  22668  lgsqrlem2  22686  gxnn0neg  23755  gxnn0suc  23756  nvmul0or  24037  hvmul0or  24432  disjxpin  25935  subfacp1lem4  27076  untsucf  27366  zprod  27455  dfon2lem6  27606  dftrpred3g  27702  wfrlem14  27742  wfrlem15  27743  nodenselem4  27830  broutsideof2  28158  btwnoutside  28161  broutsideof3  28162  outsideoftr  28165  lineunray  28183  lineelsb2  28184  meran1  28262  ontgval  28282  ordcmp  28298  mblfinlem2  28434  ovoliunnfl  28438  itg2addnclem  28448  finminlem  28518  nn0prpw  28523  refssfne  28571  sdclem2  28643  fdc  28646  divrngidl  28833  fphpdo  29161  pellfundex  29232  jm2.19lem4  29346  jm2.26a  29354  frgraogt3nreg  30718  bj-sngltag  32481  lkreqN  32820  cvrnbtwn4  32929  4atlem12  33261  elpaddn0  33449  paddasslem17  33485  paddidm  33490  pmapjoin  33501  llnexchb2  33518  dalawlem13  33532  dalawlem14  33533  dochkrshp4  35039  lcfl6  35150