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  6187  ordin  6393  fimacnvdisj  6758  f1oexrnex  7925  wemoiso  7971  wemoiso2  7972  smocdmdom  8356  rdglim  8414  oaabs  8635  ecref  8741  f1oenfi  9164  f1oenfirn  9165  f1domfi  9166  domfi  9174  sdomdomtrfi  9186  php  9192  f1vrnfibi  9300  brwdom2  9536  infdiffi  9628  cantnflem1  9659  wemapwe  9667  cnfcom3lem  9673  r1lim  9745  carduni  9968  ac5num  10021  infunsdom1  10196  cofsmo  10254  isf32lem6  10343  hsmexlem1  10411  ac6c4  10466  fnct  10522  pwfseqlem1  10644  tskuni  10769  recgt1i  12113  avgle2  12486  eluzmn  12870  rpnnen1lem1  13003  xnn0le2is012  13273  fzneuz  13638  mulmod0  13912  hasheni  14386  hashun2  14421  hashf1dmrn  14482  reccn2  15650  isershft  15717  sumeq2ii  15746  prodeq2ii  15967  demoivreALT  16258  bitsp1  16490  gcdneg  16581  eucalginv  16643  eucalg  16646  odzdvds  16856  fldivp1  16958  prmunb  16975  vdwap1  17038  setsid  17268  acsmapd  18611  intopsn  18713  cntzidss  19411  symggrp  19471  pmtrfv  19523  odmodnn0  19611  sylow2alem1  19688  telgsumfzs  20060  dprdsn  20109  dvdsrmul1  20452  dvrid  20489  cntzsubrng  20653  prmidl0  21459  znunit  21694  isphld  21785  frlmup1  21929  evl1val  22470  evl1sca  22475  pf1const  22487  mat1f1o  22616  mat1mhm  22622  matunit  22816  pm2mpmhmlem2  22957  cctop  23144  iscnp4  23401  iscncl  23407  cnntr  23413  tx2cn  23748  xkoco1cn  23795  qtopkgen  23848  hmeontr  23907  hmeores  23909  filssufilg  24049  ustuqtop1  24379  utop2nei  24388  fmucndlem  24428  cfilufg  24430  xmetres2  24499  metres2  24501  metustto  24691  metust  24696  cfilucfil  24697  dscopn  24711  nmoi  24866  iccntr  24960  cphsqrtcl2  25326  cmsss  25491  ivthlem3  25593  sca2rab  25652  ovolicc2lem3  25659  mdegleb  26202  mdegmullem  26216  aalioulem3  26478  ulm2  26529  ulmcn  26543  root1eq1  26901  atanlogsublem  27061  birthdaylem3  27099  logexprlim  27370  dchrisumlem3  27636  f1otrg  29201  ax5seglem1  29259  ax5seglem2  29260  ax5seglem3a  29261  ax5seglem4  29263  ax5seglem9  29268  ax5seg  29269  axbtwnid  29270  axlowdimlem17  29289  axcontlem2  29296  axcontlem4  29298  axcontlem8  29302  cyclnumvtx  30130  rusgrnumwwlks  30307  wwlksext2clwwlk  30389  grpoidinv  30841  imsmetlem  31023  ipasslem1  31164  ip2eqi  31189  hvpncan  31372  pjid  32028  hmopre  32256  eigvalcl  32294  leopnmid  32471  superpos  32687  cvp  32708  rabfodom  32832  xlt2addrd  33085  hashxpe  33133  suppgsumssiun  33373  cyc3genpmlem  33452  lmodslmd  33505  elrgspnlem4  33546  elrgspnsubrunlem2  33549  nsgqusf1olem2  33704  elrspunidl  33717  rsprprmprmidlb  33794  extdgfialglem1  34063  irngnminplynz  34083  constrfiss  34122  locfinreflem  34211  zarcls0  34239  fmcncfil  34302  rge0scvg  34320  esumfsup  34441  esumcvg  34457  insiga  34508  ballotlemirc  34903  signstfvcl  34941  signsvfn  34950  upgracycusgr  35628  subfacp1lem6  35658  satfdmlem  35841  msubff1  36029  fv2ndcnv  36251  matunitlindf  38250  ovoliunnfl  38294  voliunnfl  38296  volsupnfl  38297  ftc1anclem5  38329  indexa  38365  sstotbnd3  38408  heiborlem6  38448  rngosn3  38556  atlatmstc  40074  atlatle  40075  glbconN  40132  intnatN  40162  lnnat  40182  atcvrj2b  40187  atexchcvrN  40195  llncvrlpln  40313  lplncvrlvol  40371  lautcvr  40847  trlatn0  40927  cdleme48fvg  41255  cdlemg33c  41463  dihcl  42025  imadomfi  42750  fsuppssind  43308  elpell1qr2  43582  oddcomabszz  43654  wepwsolem  43752  mendring  43898  mendlmod  43899  hausgraph  43915  cantnftermord  44030  cantnfub  44031  cantnf2  44035  omabs2  44042  rp-isfinite5  44226  omelaxinf2  45681  cncmpmax  45735  eliinid  45812  icccncfext  46584  dvnprodlem2  46644  stoweidlem7  46704  stoweidlem34  46731  stoweidlem35  46732  stoweidlem59  46756  stoweidlem60  46757  stoweidlem62  46759  fourierdlem34  46838  fourierdlem73  46876  fourierdlem77  46880  etransclem35  46966  smfsuplem2  47509  pgrple2abl  49128  clddisj  49665