Theorem sylancom 599

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 489	. 2 ⊢ ((𝜑 ∧ 𝜓) → 𝜓)
3		sylancom.2	. 2 ⊢ ((𝜒 ∧ 𝜓) → 𝜃)
4	1, 2, 3	syl2anc 595	1 ⊢ ((𝜑 ∧ 𝜓) → 𝜃)

Syntax hints:   → wi 4   ∧ wa 400

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 210  df-an 401

This theorem is referenced by:  sofld  6186  ordin  6392  fimacnvdisj  6757  f1oexrnex  7923  wemoiso  7969  wemoiso2  7970  smocdmdom  8354  rdglim  8412  oaabs  8633  ecref  8739  f1oenfi  9162  f1oenfirn  9163  f1domfi  9164  domfi  9172  sdomdomtrfi  9184  php  9190  f1vrnfibi  9298  brwdom2  9534  infdiffi  9626  cantnflem1  9657  wemapwe  9665  cnfcom3lem  9671  r1lim  9743  carduni  9966  ac5num  10019  infunsdom1  10194  cofsmo  10252  isf32lem6  10341  hsmexlem1  10409  ac6c4  10464  fnct  10520  pwfseqlem1  10642  tskuni  10767  recgt1i  12111  avgle2  12484  eluzmn  12868  rpnnen1lem1  13001  xnn0le2is012  13271  fzneuz  13635  mulmod0  13909  hasheni  14383  hashun2  14418  hashf1dmrn  14479  reccn2  15647  isershft  15714  sumeq2ii  15743  prodeq2ii  15964  demoivreALT  16256  bitsp1  16488  gcdneg  16579  eucalginv  16641  eucalg  16644  odzdvds  16854  fldivp1  16956  prmunb  16973  vdwap1  17036  setsid  17266  acsmapd  18609  intopsn  18711  cntzidss  19409  symggrp  19469  pmtrfv  19521  odmodnn0  19609  sylow2alem1  19686  telgsumfzs  20058  dprdsn  20107  dvdsrmul1  20450  dvrid  20487  cntzsubrng  20651  prmidl0  21446  znunit  21681  isphld  21772  frlmup1  21916  evl1val  22457  evl1sca  22462  pf1const  22474  mat1f1o  22603  mat1mhm  22609  matunit  22803  pm2mpmhmlem2  22944  cctop  23131  iscnp4  23388  iscncl  23394  cnntr  23400  tx2cn  23735  xkoco1cn  23782  qtopkgen  23835  hmeontr  23894  hmeores  23896  filssufilg  24036  ustuqtop1  24366  utop2nei  24375  fmucndlem  24415  cfilufg  24417  xmetres2  24486  metres2  24488  metustto  24678  metust  24683  cfilucfil  24684  dscopn  24698  nmoi  24853  iccntr  24947  cphsqrtcl2  25313  cmsss  25478  ivthlem3  25580  sca2rab  25639  ovolicc2lem3  25646  mdegleb  26189  mdegmullem  26203  aalioulem3  26463  ulm2  26513  ulmcn  26527  root1eq1  26885  atanlogsublem  27045  birthdaylem3  27083  logexprlim  27354  dchrisumlem3  27620  f1otrg  29160  ax5seglem1  29218  ax5seglem2  29219  ax5seglem3a  29220  ax5seglem4  29222  ax5seglem9  29227  ax5seg  29228  axbtwnid  29229  axlowdimlem17  29248  axcontlem2  29255  axcontlem4  29257  axcontlem8  29261  cyclnumvtx  30089  rusgrnumwwlks  30266  wwlksext2clwwlk  30348  grpoidinv  30800  imsmetlem  30982  ipasslem1  31123  ip2eqi  31148  hvpncan  31331  pjid  31987  hmopre  32215  eigvalcl  32253  leopnmid  32430  superpos  32646  cvp  32667  rabfodom  32791  xlt2addrd  33044  hashxpe  33092  suppgsumssiun  33332  cyc3genpmlem  33411  lmodslmd  33464  elrgspnlem4  33505  elrgspnsubrunlem2  33508  nsgqusf1olem2  33666  elrspunidl  33679  rsprprmprmidlb  33757  extdgfialglem1  34026  irngnminplynz  34046  constrfiss  34085  locfinreflem  34174  zarcls0  34202  fmcncfil  34265  rge0scvg  34283  esumfsup  34404  esumcvg  34420  insiga  34471  ballotlemirc  34866  signstfvcl  34904  signsvfn  34913  upgracycusgr  35545  subfacp1lem6  35575  satfdmlem  35758  msubff1  35946  fv2ndcnv  36168  matunitlindf  38156  ovoliunnfl  38200  voliunnfl  38202  volsupnfl  38203  ftc1anclem5  38235  indexa  38271  sstotbnd3  38314  heiborlem6  38354  rngosn3  38462  atlatmstc  39982  atlatle  39983  glbconN  40040  intnatN  40070  lnnat  40090  atcvrj2b  40095  atexchcvrN  40103  llncvrlpln  40221  lplncvrlvol  40279  lautcvr  40755  trlatn0  40835  cdleme48fvg  41163  cdlemg33c  41371  dihcl  41933  imadomfi  42658  fsuppssind  43216  elpell1qr2  43490  oddcomabszz  43562  wepwsolem  43660  mendring  43806  mendlmod  43807  hausgraph  43823  cantnftermord  43938  cantnfub  43939  cantnf2  43943  omabs2  43950  rp-isfinite5  44134  omelaxinf2  45589  cncmpmax  45643  eliinid  45720  icccncfext  46492  dvnprodlem2  46552  stoweidlem7  46612  stoweidlem34  46639  stoweidlem35  46640  stoweidlem59  46664  stoweidlem60  46665  stoweidlem62  46667  fourierdlem34  46746  fourierdlem73  46784  fourierdlem77  46788  etransclem35  46874  smfsuplem2  47417  pgrple2abl  49029  clddisj  49566