Theorem jaod 859

Description: Deduction disjoining the antecedents of two implications. (Contributed by NM, 18-Aug-1994.)

Hypotheses

Ref	Expression
jaod.1	⊢ (𝜑 → (𝜓 → 𝜒))
jaod.2	⊢ (𝜑 → (𝜃 → 𝜒))

Assertion

Ref	Expression
jaod	⊢ (𝜑 → ((𝜓 ∨ 𝜃) → 𝜒))

Proof of Theorem jaod

Step	Hyp	Ref	Expression
1		jaod.1	. . . 4 ⊢ (𝜑 → (𝜓 → 𝜒))
2	1	com12 32	. . 3 ⊢ (𝜓 → (𝜑 → 𝜒))
3		jaod.2	. . . 4 ⊢ (𝜑 → (𝜃 → 𝜒))
4	3	com12 32	. . 3 ⊢ (𝜃 → (𝜑 → 𝜒))
5	2, 4	jaoi 857	. 2 ⊢ ((𝜓 ∨ 𝜃) → (𝜑 → 𝜒))
6	5	com12 32	1 ⊢ (𝜑 → ((𝜓 ∨ 𝜃) → 𝜒))

Syntax hints:   → wi 4   ∨ wo 847

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 207  df-or 848

This theorem is referenced by:  mpjaod  860  orel2  890  pm2.621  898  pm2.63  942  jaao  956  jaodan  959  ecase3d  1034  dedlema  1045  dedlemb  1046  cad0  1619  psssstr  4061  eqoreldif  4642  opthpr  4807  prel12g  4820  opthprneg  4821  axpr  5372  sotric  5562  sotr2  5566  sotr3  5573  relop  5799  suctr  6405  trsucss  6407  ordelinel  6420  fununi  6567  fnprb  7154  soisoi  7274  ordunisuc2  7786  poxp  8070  soxp  8071  frrlem12  8239  frrlem13  8240  tfrlem11  8319  omordi  8493  om00  8502  odi  8506  omeulem2  8510  oewordi  8519  nnmordi  8559  omsmolem  8585  swoord2  8668  nneneq  9130  dffi3  9334  inf3lem6  9542  cantnfle  9580  cantnflem1  9598  cantnflem2  9599  ttrcltr  9625  r1sdom  9686  r1ord3g  9691  rankxplim3  9793  carddom2  9889  wdomnumr  9974  alephordi  9984  alephdom  9991  cardaleph  9999  djuinf  10099  cfsuc  10167  cfsmolem  10180  sornom  10187  fin23lem25  10234  fin1a2lem11  10320  fin1a2s  10324  zorn2lem7  10412  ttukeylem5  10423  alephval2  10483  fpwwe2lem12  10553  gch2  10586  gchaclem  10589  prub  10905  sqgt0sr  11017  1re  11132  lelttr  11223  ltletr  11225  letr  11227  mul0or  11777  prodgt0  11988  mulge0b  12012  squeeze0  12045  sup2  12098  un0addcl  12434  un0mulcl  12435  nn0sub  12451  elnnz  12498  zindd  12593  rpneg  12939  xrlttri  13053  xrlelttr  13070  xrltletr  13071  xrletr  13072  qextlt  13118  qextle  13119  xmullem2  13180  xlemul1a  13203  xrsupexmnf  13220  xrinfmexpnf  13221  supxrun  13231  prunioo  13397  difreicc  13400  iccsplit  13401  uzsplit  13512  fzm1  13523  expcl2lem  13996  expeq0  14015  expnegz  14019  expaddz  14029  expmulz  14031  sqlecan  14132  facdiv  14210  facwordi  14212  bcpasc  14244  resqrex  15173  absexpz  15228  caubnd  15282  summo  15640  zsum  15641  zprod  15860  rpnnen2lem12  16150  ordvdsmul  16227  nn0rppwr  16488  nn0expgcd  16491  dvdsprime  16614  2mulprm  16620  ge2nprmge4  16628  prmdvdsexpr  16644  prmfac1  16647  pythagtriplem2  16745  4sqlem11  16883  vdwlem6  16914  vdwlem9  16917  vdwlem13  16921  cshwshashlem3  17025  prmlem0  17033  pleval2  18258  pltletr  18264  plelttr  18265  tsrlemax  18509  smndex1mgm  18832  f1omvdco2  19377  psgnunilem2  19424  efgredlemc  19674  frgpuptinv  19700  lt6abl  19824  dmdprdsplit2lem  19976  domneq0  20641  drngmul0orOLD  20694  lvecvs0or  21063  baspartn  22898  0top  22927  indistopon  22945  restntr  23126  cnindis  23236  cmpfi  23352  filconn  23827  ufprim  23853  ufildr  23875  alexsubALTlem2  23992  alexsubALTlem3  23993  alexsubALTlem4  23994  ovolicc2lem3  25476  rolle  25950  dvivthlem1  25969  coeaddlem  26210  dgrco  26237  plymul0or  26244  aalioulem3  26298  cxpge0  26648  cxpmul2z  26656  cxpcn3lem  26713  scvxcvx  26952  sqf11  27105  ppiublem1  27169  lgsdir2lem2  27293  lgsqrlem2  27314  2sqnn0  27405  2sqnn  27406  nosepon  27633  nolesgn2ores  27640  nogesgn1ores  27642  nosepne  27648  nolt02o  27663  nosupbnd1lem5  27680  madebdaylemlrcut  27895  madebday  27896  ltslpss  27904  addsproplem2  27966  leadds1  27985  addsuniflem  27997  mulsproplem9  28120  sltmuls1  28143  sltmuls2  28144  muls0ord  28181  precsexlem9  28211  precsexlem11  28213  recsex  28215  abssnid  28239  ltonold  28257  onnolt  28262  eucliddivs  28372  elnnzs  28397  expsne0  28432  bdaypw2n0bndlem  28459  bdayfinbndlem1  28463  z12zsodd  28478  lmieu  28856  upgrpredgv  29212  edglnl  29216  eucrct2eupth  30320  frgrogt3nreg  30472  nvmul0or  30725  hvmul0or  31100  snsssng  32589  disjxpin  32663  expgt0b  32897  subfacp1lem4  35377  satfvsucsuc  35559  satfrnmapom  35564  sat1el2xp  35573  gonarlem  35588  gonar  35589  goalrlem  35590  goalr  35591  fmlasucdisj  35593  satffunlem1lem1  35596  satffunlem2lem1  35598  untsucf  35904  dfon2lem6  35980  broutsideof2  36316  btwnoutside  36319  broutsideof3  36320  outsideoftr  36323  lineunray  36341  lineelsb2  36342  finminlem  36512  nn0prpw  36517  refssfne  36552  meran1  36605  ontgval  36625  ordcmp  36641  bj-sngltag  37184  bj-prmoore  37320  topdifinfindis  37551  icoreclin  37562  rdgssun  37583  finxpsuclem  37602  poimirlem24  37845  poimirlem25  37846  poimirlem29  37850  poimirlem31  37852  mblfinlem2  37859  ovoliunnfl  37863  itg2addnclem  37872  sdclem2  37943  fdc  37946  divrngidl  38229  lkreqN  39430  cvrnbtwn4  39539  4atlem12  39872  elpaddn0  40060  paddasslem17  40096  paddidm  40101  pmapjoin  40112  llnexchb2  40129  dalawlem13  40143  dalawlem14  40144  dochkrshp4  41649  lcfl6  41760  lcmineqlem  42306  primrootspoweq0  42360  aks6d1c1  42370  sticksstones22  42422  aks6d1c6lem3  42426  oexpreposd  42577  expeqidd  42580  sn-remul0ord  42663  sn-sup2  42746  fphpdo  43059  pellfundex  43128  jm2.19lem4  43234  jm2.26a  43242  ordnexbtwnsuc  43509  onov0suclim  43516  oege2  43549  succlg  43570  dflim5  43571  oacl2g  43572  omcl2  43575  omcl3g  43576  naddgeoa  43636  safesnsupfiss  43656  fzunt  43696  fzuntd  43697  fzunt1d  43698  fzuntgd  43699  relexpmulg  43951  relexp01min  43954  relexpxpmin  43958  relexpaddss  43959  clsk1indlem3  44284  or2expropbi  47280  ich2exprop  47717  poprelb  47770  reuopreuprim  47772  goldbachthlem2  47792  requad01  47867  evenltle  47963  gbowge7  48009  bgoldbtbndlem3  48053  elclnbgrelnbgr  48071  clnbgrel  48074  dfclnbgr6  48102  dfnbgr6  48103  dfsclnbgr6  48104  upgrimpths  48155  clnbgrgrim  48180  isubgr3stgrlem4  48215  isubgr3stgrlem7  48218  grlimgredgex  48246  gpgedgvtx1  48308  gpgvtxedg0  48309  gpgvtxedg1  48310  lidldomn1  48477  uzlidlring  48481  prelrrx2b  48960  line2y  49001  itschlc0xyqsol1  49012  itsclc0xyqsolr  49015  inlinecirc02plem  49032