Theorem sylancom 587

Description: Syllogism inference with commutation of antecedents. (Contributed by NM, 2-Jul-2008.)

Hypotheses

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

Assertion

Ref	Expression
sylancom	⊢ ((𝜑 ∧ 𝜓) → 𝜃)

Proof of Theorem sylancom

Step	Hyp	Ref	Expression
1		sylancom.1	. 2 ⊢ ((𝜑 ∧ 𝜓) → 𝜒)
2		simpr 484	. 2 ⊢ ((𝜑 ∧ 𝜓) → 𝜓)
3		sylancom.2	. 2 ⊢ ((𝜒 ∧ 𝜓) → 𝜃)
4	1, 2, 3	syl2anc 583	1 ⊢ ((𝜑 ∧ 𝜓) → 𝜃)

Syntax hints:   → wi 4   ∧ wa 395

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 206  df-an 396

This theorem is referenced by:  sofld  6187  ordin  6395  fimacnvdisj  6770  f1oexrnex  7921  wemoiso  7963  wemoiso2  7964  smocdmdom  8371  rdglim  8429  oaabs  8650  ssctOLD  9055  f1oenfi  9185  f1oenfirn  9186  f1domfi  9187  domfi  9195  sdomdomtrfi  9207  php  9213  onomeneqOLD  9232  f1vrnfibi  9340  brwdom2  9571  infdiffi  9656  cantnflem1  9687  wemapwe  9695  cnfcom3lem  9701  r1lim  9770  carduni  9979  ac5num  10034  infunsdom1  10211  cofsmo  10267  isf32lem6  10356  hsmexlem1  10424  ac6c4  10479  fnct  10535  pwfseqlem1  10656  tskuni  10781  recgt1i  12116  avgle2  12458  eluzmn  12834  rpnnen1lem1  12967  xnn0le2is012  13230  fzneuz  13587  mulmod0  13847  hasheni  14313  hashun2  14348  hashf1dmrn  14408  reccn2  15546  isershft  15615  sumeq2ii  15644  prodeq2ii  15862  demoivreALT  16149  bitsp1  16377  gcdneg  16468  eucalginv  16526  eucalg  16529  odzdvds  16733  fldivp1  16835  prmunb  16852  vdwap1  16915  setsid  17146  acsmapd  18512  intopsn  18580  cntzidss  19246  symggrp  19310  pmtrfv  19362  odmodnn0  19450  sylow2alem1  19527  telgsumfzs  19899  dprdsn  19948  dvdsrmul1  20261  dvrid  20298  cntzsubrng  20456  znunit  21339  isphld  21427  frlmup1  21573  evl1val  22069  evl1sca  22074  pf1const  22086  mat1f1o  22201  mat1mhm  22207  matunit  22401  pm2mpmhmlem2  22542  cctop  22730  iscnp4  22988  iscncl  22994  cnntr  23000  tx2cn  23335  xkoco1cn  23382  qtopkgen  23435  hmeontr  23494  hmeores  23496  filssufilg  23636  ustuqtop1  23967  utop2nei  23976  fmucndlem  24017  cfilufg  24019  xmetres2  24088  metres2  24090  metustto  24283  metust  24288  cfilucfil  24289  dscopn  24303  nmoi  24466  iccntr  24558  cphsqrtcl2  24935  cmsss  25100  ivthlem3  25203  sca2rab  25262  ovolicc2lem3  25269  mdegleb  25815  mdegmullem  25829  aalioulem3  26080  ulm2  26130  ulmcn  26144  root1eq1  26496  atanlogsublem  26653  birthdaylem3  26691  logexprlim  26961  dchrisumlem3  27227  f1otrg  28386  ax5seglem1  28450  ax5seglem2  28451  ax5seglem3a  28452  ax5seglem4  28454  ax5seglem9  28459  ax5seg  28460  axbtwnid  28461  axlowdimlem17  28480  axcontlem2  28487  axcontlem4  28489  axcontlem8  28493  rusgrnumwwlks  29492  wwlksext2clwwlk  29574  grpoidinv  30025  imsmetlem  30207  ipasslem1  30348  ip2eqi  30373  hvpncan  30556  pjid  31212  hmopre  31440  eigvalcl  31478  leopnmid  31655  superpos  31871  cvp  31892  rabfodom  32007  ecref  32197  xlt2addrd  32235  hashxpe  32283  cyc3genpmlem  32577  lmodslmd  32616  nsgqusf1olem2  32796  elrspunidl  32817  prmidl0  32840  irngnminplynz  33057  locfinreflem  33115  zarcls0  33143  fmcncfil  33206  rge0scvg  33224  esumfsup  33363  esumcvg  33379  insiga  33430  ballotlemirc  33825  signstfvcl  33879  signsvfn  33888  upgracycusgr  34441  subfacp1lem6  34471  satfdmlem  34654  msubff1  34842  fv2ndcnv  35050  matunitlindf  36790  ovoliunnfl  36834  voliunnfl  36836  volsupnfl  36837  ftc1anclem5  36869  indexa  36905  sstotbnd3  36948  heiborlem6  36988  rngosn3  37096  atlatmstc  38493  atlatle  38494  glbconN  38551  glbconNOLD  38552  intnatN  38582  lnnat  38602  atcvrj2b  38607  atexchcvrN  38615  llncvrlpln  38733  lplncvrlvol  38791  lautcvr  39267  trlatn0  39347  cdleme48fvg  39675  cdlemg33c  39883  dihcl  40445  fsuppssind  41468  elpell1qr2  41913  oddcomabszz  41986  wepwsolem  42087  mendring  42237  mendlmod  42238  hausgraph  42257  cantnftermord  42373  cantnfub  42374  cantnf2  42378  omabs2  42385  rp-isfinite5  42571  cncmpmax  44019  eliinid  44103  icccncfext  44903  dvnprodlem2  44963  stoweidlem7  45023  stoweidlem34  45050  stoweidlem35  45051  stoweidlem59  45075  stoweidlem60  45076  stoweidlem62  45078  fourierdlem34  45157  fourierdlem73  45195  fourierdlem77  45199  etransclem35  45285  smfsuplem2  45828  pgrple2abl  47131  clddisj  47625