Theorem jaod 860

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

Syntax hints:   → wi 4   ∨ wo 848

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 849

This theorem is referenced by:  mpjaod  861  orel2  891  pm2.621  899  pm2.63  943  jaao  957  jaodan  960  ecase3d  1035  dedlema  1046  dedlemb  1047  cad0  1620  psssstr  4050  eqoreldif  4630  opthpr  4795  prel12g  4808  opthprneg  4809  axpr  5362  sotric  5560  sotr2  5564  sotr3  5571  relop  5797  suctr  6403  trsucss  6405  ordelinel  6418  fununi  6565  fnprb  7154  soisoi  7274  ordunisuc2  7786  poxp  8069  soxp  8070  frrlem12  8238  frrlem13  8239  tfrlem11  8318  omordi  8492  om00  8501  odi  8505  omeulem2  8509  oewordi  8518  nnmordi  8558  omsmolem  8584  swoord2  8668  nneneq  9131  dffi3  9335  inf3lem6  9543  cantnfle  9581  cantnflem1  9599  cantnflem2  9600  ttrcltr  9626  r1sdom  9687  r1ord3g  9692  rankxplim3  9794  carddom2  9890  wdomnumr  9975  alephordi  9985  alephdom  9992  cardaleph  10000  djuinf  10100  cfsuc  10168  cfsmolem  10181  sornom  10188  fin23lem25  10235  fin1a2lem11  10321  fin1a2s  10325  zorn2lem7  10413  ttukeylem5  10424  alephval2  10484  fpwwe2lem12  10554  gch2  10587  gchaclem  10590  prub  10906  sqgt0sr  11018  1re  11133  lelttr  11224  ltletr  11226  letr  11228  mul0or  11778  prodgt0  11989  mulge0b  12013  squeeze0  12046  sup2  12099  un0addcl  12435  un0mulcl  12436  nn0sub  12452  elnnz  12499  zindd  12594  rpneg  12940  xrlttri  13054  xrlelttr  13071  xrltletr  13072  xrletr  13073  qextlt  13119  qextle  13120  xmullem2  13181  xlemul1a  13204  xrsupexmnf  13221  xrinfmexpnf  13222  supxrun  13232  prunioo  13398  difreicc  13401  iccsplit  13402  uzsplit  13513  fzm1  13524  expcl2lem  13997  expeq0  14016  expnegz  14020  expaddz  14030  expmulz  14032  sqlecan  14133  facdiv  14211  facwordi  14213  bcpasc  14245  resqrex  15174  absexpz  15229  caubnd  15283  summo  15641  zsum  15642  zprod  15861  rpnnen2lem12  16151  ordvdsmul  16228  nn0rppwr  16489  nn0expgcd  16492  dvdsprime  16615  2mulprm  16621  ge2nprmge4  16629  prmdvdsexpr  16645  prmfac1  16648  pythagtriplem2  16746  4sqlem11  16884  vdwlem6  16915  vdwlem9  16918  vdwlem13  16922  cshwshashlem3  17026  prmlem0  17034  pleval2  18259  pltletr  18265  plelttr  18266  tsrlemax  18510  smndex1mgm  18836  f1omvdco2  19381  psgnunilem2  19428  efgredlemc  19678  frgpuptinv  19704  lt6abl  19828  dmdprdsplit2lem  19980  domneq0  20643  drngmul0orOLD  20696  lvecvs0or  21065  baspartn  22897  0top  22926  indistopon  22944  restntr  23125  cnindis  23235  cmpfi  23351  filconn  23826  ufprim  23852  ufildr  23874  alexsubALTlem2  23991  alexsubALTlem3  23992  alexsubALTlem4  23993  ovolicc2lem3  25464  rolle  25935  dvivthlem1  25954  coeaddlem  26195  dgrco  26221  plymul0or  26228  aalioulem3  26282  cxpge0  26632  cxpmul2z  26640  cxpcn3lem  26697  scvxcvx  26936  sqf11  27089  ppiublem1  27153  lgsdir2lem2  27277  lgsqrlem2  27298  2sqnn0  27389  2sqnn  27390  nosepon  27617  nolesgn2ores  27624  nogesgn1ores  27626  nosepne  27632  nolt02o  27647  nosupbnd1lem5  27664  madebdaylemlrcut  27879  madebday  27880  ltslpss  27888  addsproplem2  27950  leadds1  27969  addsuniflem  27981  mulsproplem9  28104  sltmuls1  28127  sltmuls2  28128  muls0ord  28165  precsexlem9  28195  precsexlem11  28197  recsex  28199  abssnid  28223  ltonold  28241  onnolt  28246  eucliddivs  28356  elnnzs  28381  expsne0  28416  bdaypw2n0bndlem  28443  bdayfinbndlem1  28447  z12zsodd  28462  lmieu  28840  upgrpredgv  29196  edglnl  29200  eucrct2eupth  30304  frgrogt3nreg  30456  nvmul0or  30710  hvmul0or  31085  snsssng  32573  disjxpin  32647  expgt0b  32880  axprALT2  35259  subfacp1lem4  35371  satfvsucsuc  35553  satfrnmapom  35558  sat1el2xp  35567  gonarlem  35582  gonar  35583  goalrlem  35584  goalr  35585  fmlasucdisj  35587  satffunlem1lem1  35590  satffunlem2lem1  35592  untsucf  35898  dfon2lem6  35974  broutsideof2  36310  btwnoutside  36313  broutsideof3  36314  outsideoftr  36317  lineunray  36335  lineelsb2  36336  finminlem  36506  nn0prpw  36511  refssfne  36546  meran1  36599  ontgval  36619  ordcmp  36635  axtcond  36666  bj-sngltag  37288  bj-axseprep  37379  bj-prmoore  37425  topdifinfindis  37658  icoreclin  37669  rdgssun  37690  finxpsuclem  37709  poimirlem24  37956  poimirlem25  37957  poimirlem29  37961  poimirlem31  37963  mblfinlem2  37970  ovoliunnfl  37974  itg2addnclem  37983  sdclem2  38054  fdc  38057  divrngidl  38340  lkreqN  39607  cvrnbtwn4  39716  4atlem12  40049  elpaddn0  40237  paddasslem17  40273  paddidm  40278  pmapjoin  40289  llnexchb2  40306  dalawlem13  40320  dalawlem14  40321  dochkrshp4  41826  lcfl6  41937  lcmineqlem  42483  primrootspoweq0  42537  aks6d1c1  42547  sticksstones22  42599  aks6d1c6lem3  42603  oexpreposd  42753  expeqidd  42756  sn-remul0ord  42839  sn-sup2  42935  fphpdo  43248  pellfundex  43317  jm2.19lem4  43423  jm2.26a  43431  ordnexbtwnsuc  43698  onov0suclim  43705  oege2  43738  succlg  43759  dflim5  43760  oacl2g  43761  omcl2  43764  omcl3g  43765  naddgeoa  43825  safesnsupfiss  43845  fzunt  43885  fzuntd  43886  fzunt1d  43887  fzuntgd  43888  relexpmulg  44140  relexp01min  44143  relexpxpmin  44147  relexpaddss  44148  clsk1indlem3  44473  or2expropbi  47468  ich2exprop  47905  poprelb  47958  reuopreuprim  47960  goldbachthlem2  47980  requad01  48055  evenltle  48151  gbowge7  48197  bgoldbtbndlem3  48241  elclnbgrelnbgr  48259  clnbgrel  48262  dfclnbgr6  48290  dfnbgr6  48291  dfsclnbgr6  48292  upgrimpths  48343  clnbgrgrim  48368  isubgr3stgrlem4  48403  isubgr3stgrlem7  48406  grlimgredgex  48434  gpgedgvtx1  48496  gpgvtxedg0  48497  gpgvtxedg1  48498  lidldomn1  48665  uzlidlring  48669  prelrrx2b  49148  line2y  49189  itschlc0xyqsol1  49200  itsclc0xyqsolr  49203  inlinecirc02plem  49220