Theorem jaod 865

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 863	. 2 ⊢ ((𝜓 ∨ 𝜃) → (𝜑 → 𝜒))
6	5	com12 32	1 ⊢ (𝜑 → ((𝜓 ∨ 𝜃) → 𝜒))

Syntax hints:   → wi 4   ∨ wo 853

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 208  df-or 854

This theorem is referenced by:  mpjaod  866  orel2  896  pm2.621  904  pm2.63  948  jaao  962  jaodan  965  ecase3d  1040  dedlema  1051  dedlemb  1052  cad0  1625  psssstr  4047  eqoreldif  4624  opthpr  4789  prel12g  4802  opthprneg  4803  axpr  5363  sotric  5563  sotr2  5567  sotr3  5574  relop  5799  suctr  6405  trsucss  6407  ordelinel  6420  fununi  6567  fnprb  7159  soisoi  7279  ordunisuc2  7791  poxp  8075  soxp  8076  frrlem12  8244  frrlem13  8245  tfrlem11  8324  omordi  8498  om00  8507  odi  8511  omeulem2  8515  oewordi  8524  nnmordi  8564  omsmolem  8590  swoord2  8674  nneneq  9137  dffi3  9341  inf3lem6  9552  cantnfle  9590  cantnflem1  9608  cantnflem2  9609  ttrcltr  9635  r1sdom  9696  r1ord3g  9701  rankxplim3  9803  carddom2  9899  wdomnumr  9984  alephordi  9994  alephdom  10001  cardaleph  10009  djuinf  10109  cfsuc  10177  cfsmolem  10190  sornom  10197  fin23lem25  10244  fin1a2lem11  10330  fin1a2s  10334  zorn2lem7  10422  ttukeylem5  10433  alephval2  10493  fpwwe2lem12  10563  gch2  10596  gchaclem  10599  prub  10915  sqgt0sr  11027  1re  11142  lelttr  11234  ltletr  11236  letr  11238  mul0or  11788  prodgt0  12000  mulge0b  12024  squeeze0  12057  sup2  12110  un0addcl  12468  un0mulcl  12469  nn0sub  12485  elnnz  12532  zindd  12628  rpneg  12974  xrlttri  13088  xrlelttr  13105  xrltletr  13106  xrletr  13107  qextlt  13153  qextle  13154  xmullem2  13215  xlemul1a  13238  xrsupexmnf  13255  xrinfmexpnf  13256  supxrun  13266  prunioo  13432  difreicc  13435  iccsplit  13436  uzsplit  13548  fzm1  13559  expcl2lem  14033  expeq0  14052  expnegz  14056  expaddz  14066  expmulz  14068  sqlecan  14169  facdiv  14247  facwordi  14249  bcpasc  14281  resqrex  15210  absexpz  15265  caubnd  15319  summo  15677  zsum  15678  zprod  15900  rpnnen2lem12  16190  ordvdsmul  16267  nn0rppwr  16528  nn0expgcd  16531  dvdsprime  16654  2mulprm  16660  ge2nprmge4  16669  prmdvdsexpr  16685  prmfac1  16688  pythagtriplem2  16786  4sqlem11  16924  vdwlem6  16955  vdwlem9  16958  vdwlem13  16962  cshwshashlem3  17066  prmlem0  17074  pleval2  18299  pltletr  18305  plelttr  18306  tsrlemax  18550  smndex1mgm  18876  f1omvdco2  19421  psgnunilem2  19468  efgredlemc  19718  frgpuptinv  19744  lt6abl  19868  dmdprdsplit2lem  20020  domneq0  20687  drngmul0orOLD  20740  lvecvs0or  21108  baspartn  22944  0top  22973  indistopon  22991  restntr  23172  cnindis  23282  cmpfi  23398  filconn  23873  ufprim  23899  ufildr  23921  alexsubALTlem2  24038  alexsubALTlem3  24039  alexsubALTlem4  24040  ovolicc2lem3  25511  rolle  25982  dvivthlem1  26000  coeaddlem  26239  dgrco  26265  plymul0or  26272  aalioulem3  26325  cxpge0  26672  cxpmul2z  26680  cxpcn3lem  26736  scvxcvx  26974  sqf11  27127  ppiublem1  27190  lgsdir2lem2  27314  lgsqrlem2  27335  2sqnn0  27426  2sqnn  27427  nosepon  27654  nolesgn2ores  27661  nogesgn1ores  27663  nosepne  27669  nolt02o  27684  nosupbnd1lem5  27701  madebdaylemlrcut  27916  madebday  27917  ltslpss  27925  addsproplem2  27987  leadds1  28006  addsuniflem  28018  mulsproplem9  28141  sltmuls1  28164  sltmuls2  28165  muls0ord  28202  precsexlem9  28232  precsexlem11  28234  recsex  28236  abssnid  28260  ltonold  28278  onnolt  28283  eucliddivs  28393  elnnzs  28418  expsne0  28453  bdaypw2n0bndlem  28480  bdayfinbndlem1  28484  z12zsodd  28499  lmieu  28877  upgrpredgv  29233  edglnl  29237  eucrct2eupth  30340  frgrogt3nreg  30492  nvmul0or  30746  hvmul0or  31121  snsssng  32609  disjxpin  32684  expgt0b  32916  axprALT2  35297  subfacp1lem4  35418  satfvsucsuc  35600  satfrnmapom  35605  sat1el2xp  35614  gonarlem  35629  gonar  35630  goalrlem  35631  goalr  35632  fmlasucdisj  35634  satffunlem1lem1  35637  satffunlem2lem1  35639  untsucf  35945  dfon2lem6  36021  broutsideof2  36357  btwnoutside  36360  broutsideof3  36361  outsideoftr  36364  lineunray  36382  lineelsb2  36383  finminlem  36553  nn0prpw  36558  refssfne  36593  meran1  36646  ontgval  36666  ordcmp  36682  axtcond  36713  mh-inf3f1  36776  bj-sngltag  37343  bj-axseprep  37434  bj-prmoore  37480  topdifinfindis  37715  icoreclin  37726  rdgssun  37747  finxpsuclem  37766  poimirlem24  38018  poimirlem25  38019  poimirlem29  38023  poimirlem31  38025  mblfinlem2  38032  ovoliunnfl  38036  itg2addnclem  38045  sdclem2  38116  fdc  38119  divrngidl  38402  lkreqN  39669  cvrnbtwn4  39778  4atlem12  40111  elpaddn0  40299  paddasslem17  40335  paddidm  40340  pmapjoin  40351  llnexchb2  40368  dalawlem13  40382  dalawlem14  40383  dochkrshp4  41888  lcfl6  41999  lcmineqlem  42544  primrootspoweq0  42598  aks6d1c1  42608  sticksstones22  42660  aks6d1c6lem3  42664  oexpreposd  42806  expeqidd  42809  sn-remul0ord  42892  sn-sup2  42988  fphpdo  43269  pellfundex  43338  jm2.19lem4  43444  jm2.26a  43452  ordnexbtwnsuc  43719  onov0suclim  43726  oege2  43759  succlg  43780  dflim5  43781  oacl2g  43782  omcl2  43785  omcl3g  43786  naddgeoa  43846  safesnsupfiss  43866  fzunt  43906  fzuntd  43907  fzunt1d  43908  fzuntgd  43909  relexpmulg  44161  relexp01min  44164  relexpxpmin  44168  relexpaddss  44169  clsk1indlem3  44494  or2expropbi  47504  ich2exprop  47953  poprelb  48006  reuopreuprim  48008  goldbachthlem2  48031  nprmdvdsfacm1lem2  48106  nprmdvdsfacm1  48109  requad01  48119  evenltle  48215  gbowge7  48261  bgoldbtbndlem3  48305  elclnbgrelnbgr  48323  clnbgrel  48326  dfclnbgr6  48354  dfnbgr6  48355  dfsclnbgr6  48356  upgrimpths  48407  clnbgrgrim  48432  isubgr3stgrlem4  48467  isubgr3stgrlem7  48470  grlimgredgex  48498  gpgedgvtx1  48560  gpgvtxedg0  48561  gpgvtxedg1  48562  lidldomn1  48729  uzlidlring  48733  prelrrx2b  49212  line2y  49253  itschlc0xyqsol1  49264  itsclc0xyqsolr  49267  inlinecirc02plem  49284