Theorem sylancom 588

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 584	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 207  df-an 396

This theorem is referenced by:  sofld  6136  ordin  6337  fimacnvdisj  6702  f1oexrnex  7860  wemoiso  7908  wemoiso2  7909  smocdmdom  8291  rdglim  8348  oaabs  8566  ecref  8670  f1oenfi  9093  f1oenfirn  9094  f1domfi  9095  domfi  9103  sdomdomtrfi  9115  php  9121  f1vrnfibi  9232  brwdom2  9465  infdiffi  9554  cantnflem1  9585  wemapwe  9593  cnfcom3lem  9599  r1lim  9668  carduni  9877  ac5num  9930  infunsdom1  10106  cofsmo  10163  isf32lem6  10252  hsmexlem1  10320  ac6c4  10375  fnct  10431  pwfseqlem1  10552  tskuni  10677  recgt1i  12022  avgle2  12365  eluzmn  12742  rpnnen1lem1  12879  xnn0le2is012  13148  fzneuz  13511  mulmod0  13781  hasheni  14255  hashun2  14290  hashf1dmrn  14350  reccn2  15504  isershft  15571  sumeq2ii  15600  prodeq2ii  15818  demoivreALT  16110  bitsp1  16342  gcdneg  16433  eucalginv  16495  eucalg  16498  odzdvds  16707  fldivp1  16809  prmunb  16826  vdwap1  16889  setsid  17118  acsmapd  18460  intopsn  18528  cntzidss  19219  symggrp  19279  pmtrfv  19331  odmodnn0  19419  sylow2alem1  19496  telgsumfzs  19868  dprdsn  19917  dvdsrmul1  20254  dvrid  20291  cntzsubrng  20452  znunit  21470  isphld  21561  frlmup1  21705  evl1val  22214  evl1sca  22219  pf1const  22231  mat1f1o  22363  mat1mhm  22369  matunit  22563  pm2mpmhmlem2  22704  cctop  22891  iscnp4  23148  iscncl  23154  cnntr  23160  tx2cn  23495  xkoco1cn  23542  qtopkgen  23595  hmeontr  23654  hmeores  23656  filssufilg  23796  ustuqtop1  24127  utop2nei  24136  fmucndlem  24176  cfilufg  24178  xmetres2  24247  metres2  24249  metustto  24439  metust  24444  cfilucfil  24445  dscopn  24459  nmoi  24614  iccntr  24708  cphsqrtcl2  25084  cmsss  25249  ivthlem3  25352  sca2rab  25411  ovolicc2lem3  25418  mdegleb  25967  mdegmullem  25981  aalioulem3  26240  ulm2  26292  ulmcn  26306  root1eq1  26663  atanlogsublem  26823  birthdaylem3  26861  logexprlim  27134  dchrisumlem3  27400  f1otrg  28816  ax5seglem1  28873  ax5seglem2  28874  ax5seglem3a  28875  ax5seglem4  28877  ax5seglem9  28882  ax5seg  28883  axbtwnid  28884  axlowdimlem17  28903  axcontlem2  28910  axcontlem4  28912  axcontlem8  28916  cyclnumvtx  29745  rusgrnumwwlks  29919  wwlksext2clwwlk  30001  grpoidinv  30452  imsmetlem  30634  ipasslem1  30775  ip2eqi  30800  hvpncan  30983  pjid  31639  hmopre  31867  eigvalcl  31905  leopnmid  32082  superpos  32298  cvp  32319  rabfodom  32449  xlt2addrd  32702  hashxpe  32752  cyc3genpmlem  33093  lmodslmd  33146  elrgspnlem4  33185  elrgspnsubrunlem2  33188  nsgqusf1olem2  33351  elrspunidl  33365  prmidl0  33387  rsprprmprmidlb  33460  extdgfialglem1  33659  irngnminplynz  33679  constrfiss  33718  locfinreflem  33807  zarcls0  33835  fmcncfil  33898  rge0scvg  33916  esumfsup  34037  esumcvg  34053  insiga  34104  ballotlemirc  34500  signstfvcl  34541  signsvfn  34550  upgracycusgr  35128  subfacp1lem6  35158  satfdmlem  35341  msubff1  35529  fv2ndcnv  35751  matunitlindf  37598  ovoliunnfl  37642  voliunnfl  37644  volsupnfl  37645  ftc1anclem5  37677  indexa  37713  sstotbnd3  37756  heiborlem6  37796  rngosn3  37904  atlatmstc  39298  atlatle  39299  glbconN  39356  intnatN  39386  lnnat  39406  atcvrj2b  39411  atexchcvrN  39419  llncvrlpln  39537  lplncvrlvol  39595  lautcvr  40071  trlatn0  40151  cdleme48fvg  40479  cdlemg33c  40687  dihcl  41249  imadomfi  41975  fsuppssind  42566  elpell1qr2  42845  oddcomabszz  42917  wepwsolem  43015  mendring  43161  mendlmod  43162  hausgraph  43178  cantnftermord  43293  cantnfub  43294  cantnf2  43298  omabs2  43305  rp-isfinite5  43490  omelaxinf2  44963  cncmpmax  45010  eliinid  45089  icccncfext  45868  dvnprodlem2  45928  stoweidlem7  45988  stoweidlem34  46015  stoweidlem35  46016  stoweidlem59  46040  stoweidlem60  46041  stoweidlem62  46043  fourierdlem34  46122  fourierdlem73  46160  fourierdlem77  46164  etransclem35  46250  smfsuplem2  46793  pgrple2abl  48349  clddisj  48888