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  1614  psssstr  4118  eqoreldif  4689  opthpr  4855  prel12g  4868  opthprneg  4869  axpr  5432  sotric  5625  sotr2  5629  sotr3  5636  relop  5863  suctr  6471  trsucss  6473  ordelinel  6486  fununi  6642  fnprb  7227  soisoi  7347  ordunisuc2  7864  poxp  8151  soxp  8152  frrlem12  8320  frrlem13  8321  wfrlem14OLD  8360  wfrlem15OLD  8361  tfrlem11  8426  omordi  8602  om00  8611  odi  8615  omeulem2  8619  oewordi  8627  nnmordi  8667  omsmolem  8693  swoord2  8776  nneneq  9243  nneneqOLD  9255  dffi3  9468  inf3lem6  9670  cantnfle  9708  cantnflem1  9726  cantnflem2  9727  ttrcltr  9753  r1sdom  9811  r1ord3g  9816  rankxplim3  9918  carddom2  10014  wdomnumr  10101  alephordi  10111  alephdom  10118  cardaleph  10126  djuinf  10226  cfsuc  10294  cfsmolem  10307  sornom  10314  fin23lem25  10361  fin1a2lem11  10447  fin1a2s  10451  zorn2lem7  10539  ttukeylem5  10550  alephval2  10609  fpwwe2lem12  10679  gch2  10712  gchaclem  10715  prub  11031  sqgt0sr  11143  1re  11258  lelttr  11348  ltletr  11350  letr  11352  mul0or  11900  prodgt0  12111  mulge0b  12135  squeeze0  12168  sup2  12221  un0addcl  12556  un0mulcl  12557  nn0sub  12573  elnnz  12620  zindd  12716  rpneg  13064  xrlttri  13177  xrlelttr  13194  xrltletr  13195  xrletr  13196  qextlt  13241  qextle  13242  xmullem2  13303  xlemul1a  13326  xrsupexmnf  13343  xrinfmexpnf  13344  supxrun  13354  prunioo  13517  difreicc  13520  iccsplit  13521  uzsplit  13632  fzm1  13643  expcl2lem  14110  expeq0  14129  expnegz  14133  expaddz  14143  expmulz  14145  sqlecan  14244  facdiv  14322  facwordi  14324  bcpasc  14356  resqrex  15285  absexpz  15340  caubnd  15393  summo  15749  zsum  15750  zprod  15969  rpnnen2lem12  16257  ordvdsmul  16333  nn0rppwr  16594  nn0expgcd  16597  dvdsprime  16720  2mulprm  16726  ge2nprmge4  16734  prmdvdsexpr  16750  prmfac1  16753  pythagtriplem2  16850  4sqlem11  16988  vdwlem6  17019  vdwlem9  17022  vdwlem13  17026  cshwshashlem3  17131  prmlem0  17139  pleval2  18394  pltletr  18400  plelttr  18401  tsrlemax  18643  smndex1mgm  18932  f1omvdco2  19480  psgnunilem2  19527  efgredlemc  19777  frgpuptinv  19803  lt6abl  19927  dmdprdsplit2lem  20079  domneq0  20724  drngmul0orOLD  20777  lvecvs0or  21127  baspartn  22976  0top  23005  indistopon  23023  restntr  23205  cnindis  23315  cmpfi  23431  filconn  23906  ufprim  23932  ufildr  23954  alexsubALTlem2  24071  alexsubALTlem3  24072  alexsubALTlem4  24073  ovolicc2lem3  25567  rolle  26042  dvivthlem1  26061  coeaddlem  26302  dgrco  26329  plymul0or  26336  aalioulem3  26390  cxpge0  26739  cxpmul2z  26747  cxpcn3lem  26804  scvxcvx  27043  sqf11  27196  ppiublem1  27260  lgsdir2lem2  27384  lgsqrlem2  27405  2sqnn0  27496  2sqnn  27497  nosepon  27724  nolesgn2ores  27731  nogesgn1ores  27733  nosepne  27739  nolt02o  27754  nosupbnd1lem5  27771  madebdaylemlrcut  27951  madebday  27952  sltlpss  27959  addsproplem2  28017  sleadd1  28036  addsuniflem  28048  mulsproplem9  28164  ssltmul1  28187  ssltmul2  28188  muls0ord  28225  precsexlem9  28253  precsexlem11  28255  recsex  28257  abssnid  28281  sltonold  28297  elnnzs  28401  expsne0  28428  zs12bday  28438  lmieu  28806  upgrpredgv  29170  edglnl  29174  eucrct2eupth  30273  frgrogt3nreg  30425  nvmul0or  30678  hvmul0or  31053  snsssng  32541  disjxpin  32607  expgt0b  32822  subfacp1lem4  35167  satfvsucsuc  35349  satfrnmapom  35354  sat1el2xp  35363  gonarlem  35378  gonar  35379  goalrlem  35380  goalr  35381  fmlasucdisj  35383  satffunlem1lem1  35386  satffunlem2lem1  35388  untsucf  35689  dfon2lem6  35769  broutsideof2  36103  btwnoutside  36106  broutsideof3  36107  outsideoftr  36110  lineunray  36128  lineelsb2  36129  finminlem  36300  nn0prpw  36305  refssfne  36340  meran1  36393  ontgval  36413  ordcmp  36429  bj-sngltag  36965  bj-prmoore  37097  topdifinfindis  37328  icoreclin  37339  rdgssun  37360  finxpsuclem  37379  poimirlem24  37630  poimirlem25  37631  poimirlem29  37635  poimirlem31  37637  mblfinlem2  37644  ovoliunnfl  37648  itg2addnclem  37657  sdclem2  37728  fdc  37731  divrngidl  38014  lkreqN  39151  cvrnbtwn4  39260  4atlem12  39594  elpaddn0  39782  paddasslem17  39818  paddidm  39823  pmapjoin  39834  llnexchb2  39851  dalawlem13  39865  dalawlem14  39866  dochkrshp4  41371  lcfl6  41482  lcmineqlem  42033  primrootspoweq0  42087  aks6d1c1  42097  sticksstones22  42149  aks6d1c6lem3  42153  oexpreposd  42335  expeqidd  42338  sn-sup2  42477  fphpdo  42804  pellfundex  42873  jm2.19lem4  42980  jm2.26a  42988  ordnexbtwnsuc  43256  onov0suclim  43263  oege2  43296  succlg  43317  dflim5  43318  oacl2g  43319  omcl2  43322  omcl3g  43323  naddgeoa  43383  safesnsupfiss  43404  fzunt  43444  fzuntd  43445  fzunt1d  43446  fzuntgd  43447  relexpmulg  43699  relexp01min  43702  relexpxpmin  43706  relexpaddss  43707  clsk1indlem3  44032  or2expropbi  46983  ich2exprop  47395  poprelb  47448  reuopreuprim  47450  goldbachthlem2  47470  requad01  47545  evenltle  47641  gbowge7  47687  bgoldbtbndlem3  47731  elclnbgrelnbgr  47749  clnbgrel  47752  dfclnbgr6  47779  dfnbgr6  47780  dfsclnbgr6  47781  clnbgrgrim  47839  isubgr3stgrlem4  47871  isubgr3stgrlem7  47874  gpgedgvtx1  47954  gpgvtxedg0  47955  gpgvtxedg1  47956  lidldomn1  48074  uzlidlring  48078  prelrrx2b  48563  line2y  48604  itschlc0xyqsol1  48615  itsclc0xyqsolr  48618  inlinecirc02plem  48635