Theorem jaod 386

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

Syntax hints:   -> wi 4   \/ wo 374

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 190  df-or 376

This theorem is referenced by:  mpjaod  387  orel2  389  pm2.621  414  jaao  516  jaodan  799  pm2.63  802  ecase2d  957  ecase3d  960  dedlema  971  dedlemb  972  cad0  1531  psssstr  3551  opthpr  4166  sotric  4800  sotr2  4803  relop  5004  trsucss  5527  ordelinel  5540  fununi  5671  fnprb  6147  soisoi  6244  ordunisuc2  6698  poxp  6935  soxp  6936  wfrlem14  7075  wfrlem15  7076  tfrlem11  7132  omordi  7293  om00  7302  odi  7306  omeulem2  7310  oewordi  7318  nnmordi  7358  omsmolem  7380  swoord2  7419  nneneq  7781  dffi3  7971  inf3lem6  8164  cantnfle  8202  cantnflem1  8220  cantnflem2  8221  r1sdom  8271  r1ord3g  8276  rankxplim3  8378  carddom2  8437  wdomnumr  8521  alephordi  8531  alephdom  8538  cardaleph  8546  cdainf  8648  cfsuc  8713  cfsmolem  8726  sornom  8733  fin23lem25  8780  fin1a2lem11  8866  fin1a2s  8870  zorn2lem7  8958  ttukeylem5  8969  alephval2  9023  fpwwe2lem13  9093  gch2  9126  gchaclem  9129  prub  9445  sqgt0sr  9556  1re  9668  lelttr  9750  ltletr  9751  letr  9753  mul0or  10280  prodgt0  10478  mulge0b  10503  squeeze0  10537  sup2  10593  un0addcl  10932  un0mulcl  10933  nn0sub  10949  elnnz  10976  zindd  11065  rpneg  11361  xrlttri  11467  xrlelttr  11482  xrltletr  11483  xrletr  11484  qextlt  11525  qextle  11526  xmullem2  11580  xlemul1a  11603  xrsupexmnf  11619  xrinfmexpnf  11620  supxrun  11630  prunioo  11790  difreicc  11793  iccsplit  11794  uzsplit  11895  fzm1  11903  expcl2lem  12316  expeq0  12334  expnegz  12338  expaddz  12348  expmulz  12350  sqlecan  12413  facdiv  12504  facwordi  12506  bcpasc  12538  resqrex  13363  absexpz  13417  caubnd  13470  summo  13832  zsum  13833  zprod  14040  rpnnen2  14327  ordvdsmul  14390  dvdsprime  14686  prmdvdsexpr  14718  prmfac1  14720  pythagtriplem2  14816  4sqlem11  14948  vdwlem6  14985  vdwlem9  14988  vdwlem13  14992  cshwshashlem3  15117  prmlem0  15126  xpscfv  15517  pleval2  16260  pltletr  16266  plelttr  16267  tsrlemax  16515  f1omvdco2  17138  psgnunilem2  17185  efgredlemc  17444  frgpuptinv  17470  lt6abl  17578  dmdprdsplit2lem  17727  drngmul0or  18045  lvecvs0or  18380  domneq0  18570  baspartn  20018  0top  20048  indistopon  20065  restntr  20247  cnindis  20357  cmpfi  20472  filcon  20947  ufprim  20973  ufildr  20995  alexsubALTlem2  21112  alexsubALTlem3  21113  alexsubALTlem4  21114  ovolicc2lem3  22521  rolle  22991  dvivthlem1  23009  coeaddlem  23252  dgrco  23278  plymul0or  23283  aalioulem3  23339  cxpge0  23677  cxpmul2z  23685  cxpcn3lem  23736  scvxcvx  23960  sqf11  24115  ppiublem1  24179  lgsdir2lem2  24301  lgsqrlem2  24319  lmieu  24875  frgraogt3nreg  25897  gxnn0neg  26040  gxnn0suc  26041  nvmul0or  26322  hvmul0or  26727  disjxpin  28247  subfacp1lem4  29955  untsucf  30386  dfon2lem6  30483  dftrpred3g  30523  nosepon  30605  nodenselem4  30622  broutsideof2  30938  btwnoutside  30941  broutsideof3  30942  outsideoftr  30945  lineunray  30963  lineelsb2  30964  finminlem  31023  nn0prpw  31028  refssfne  31063  meran1  31120  ontgval  31140  ordcmp  31156  bj-sngltag  31622  topdifinfindis  31794  icoreclin  31805  finxpsuclem  31834  poimirlem24  32009  poimirlem25  32010  poimirlem29  32014  poimirlem31  32016  mblfinlem2  32023  ovoliunnfl  32027  itg2addnclem  32038  sdclem2  32116  fdc  32119  divrngidl  32306  lkreqN  32781  cvrnbtwn4  32890  4atlem12  33222  elpaddn0  33410  paddasslem17  33446  paddidm  33451  pmapjoin  33462  llnexchb2  33479  dalawlem13  33493  dalawlem14  33494  dochkrshp4  35002  lcfl6  35113  fphpdo  35705  pellfundex  35779  jm2.19lem4  35892  jm2.26a  35900  relexpmulg  36347  relexp01min  36350  relexpxpmin  36354  relexpaddss  36355  gboge7  38902  bgoldbtbndlem3  38940  upgredg  39276  lidldomn1  40194  uzlidlring  40202