Theorem sylancom 600

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  sofld  6187  ordin  6395  fimacnvdisj  6760  f1oexrnex  7926  wemoiso  7972  wemoiso2  7973  smocdmdom  8357  rdglim  8415  oaabs  8636  ecref  8742  f1oenfi  9166  f1oenfirn  9167  f1domfi  9168  domfi  9176  sdomdomtrfi  9188  php  9194  f1vrnfibi  9302  brwdom2  9538  infdiffi  9630  cantnflem1  9661  wemapwe  9669  cnfcom3lem  9675  r1lim  9747  carduni  9979  ac5num  10032  infunsdom1  10207  cofsmo  10264  isf32lem6  10353  hsmexlem1  10421  ac6c4  10476  fnct  10532  pwfseqlem1  10654  tskuni  10779  recgt1i  12123  avgle2  12496  eluzmn  12880  rpnnen1lem1  13013  xnn0le2is012  13283  fzneuz  13648  mulmod0  13923  hasheni  14397  hashun2  14432  hashf1dmrn  14493  reccn2  15667  isershft  15734  sumeq2ii  15763  prodeq2ii  15983  demoivreALT  16274  bitsp1  16506  gcdneg  16597  eucalginv  16659  eucalg  16662  odzdvds  16872  fldivp1  16974  prmunb  16991  vdwap1  17054  setsid  17284  acsmapd  18627  intopsn  18729  cntzidss  19433  symggrp  19493  pmtrfv  19545  odmodnn0  19633  sylow2alem1  19710  telgsumfzs  20082  dprdsn  20131  dvdsrmul1  20476  dvrid  20513  cntzsubrng  20695  prmidl0  21507  znunit  21742  isphld  21833  frlmup1  21977  evl1val  22518  evl1sca  22523  pf1const  22535  mat1f1o  22664  mat1mhm  22670  matunit  22864  pm2mpmhmlem2  23005  cctop  23192  iscnp4  23449  iscncl  23455  cnntr  23461  tx2cn  23796  xkoco1cn  23843  qtopkgen  23896  hmeontr  23955  hmeores  23957  filssufilg  24097  ustuqtop1  24427  utop2nei  24436  fmucndlem  24476  cfilufg  24478  xmetres2  24547  metres2  24549  metustto  24739  metust  24744  cfilucfil  24745  dscopn  24759  nmoi  24914  iccntr  25008  cphsqrtcl2  25374  cmsss  25539  ivthlem3  25641  sca2rab  25700  ovolicc2lem3  25707  mdegleb  26250  mdegmullem  26264  aalioulem3  26526  ulm2  26577  ulmcn  26591  root1eq1  26949  atanlogsublem  27109  birthdaylem3  27147  logexprlim  27418  dchrisumlem3  27684  f1otrg  29249  ax5seglem1  29307  ax5seglem2  29308  ax5seglem3a  29309  ax5seglem4  29311  ax5seglem9  29316  ax5seg  29317  axbtwnid  29318  axlowdimlem17  29337  axcontlem2  29344  axcontlem4  29346  axcontlem8  29350  cyclnumvtx  30178  rusgrnumwwlks  30355  wwlksext2clwwlk  30437  grpoidinv  30889  imsmetlem  31071  ipasslem1  31212  ip2eqi  31237  hvpncan  31420  pjid  32076  hmopre  32304  eigvalcl  32342  leopnmid  32519  superpos  32735  cvp  32756  rabfodom  32880  xlt2addrd  33133  hashxpe  33181  suppgsumssiun  33415  cyc3genpmlem  33494  lmodslmd  33547  elrgspnlem4  33588  elrgspnsubrunlem2  33591  nsgqusf1olem2  33746  elrspunidl  33759  rsprprmprmidlb  33836  extdgfialglem1  34105  irngnminplynz  34125  constrfiss  34164  locfinreflem  34253  zarcls0  34281  fmcncfil  34344  rge0scvg  34362  esumfsup  34483  esumcvg  34499  insiga  34551  ballotlemirc  34946  signstfvcl  34984  signsvfn  34993  upgracycusgr  35660  subfacp1lem6  35690  satfdmlem  35873  msubff1  36061  fv2ndcnv  36283  matunitlindf  38302  ovoliunnfl  38346  voliunnfl  38348  volsupnfl  38349  ftc1anclem5  38381  indexa  38417  sstotbnd3  38460  heiborlem6  38500  rngosn3  38608  atlatmstc  40126  atlatle  40127  glbconN  40184  intnatN  40214  lnnat  40234  atcvrj2b  40239  atexchcvrN  40247  llncvrlpln  40365  lplncvrlvol  40423  lautcvr  40899  trlatn0  40979  cdleme48fvg  41307  cdlemg33c  41515  dihcl  42077  imadomfi  42802  fsuppssind  43358  elpell1qr2  43632  oddcomabszz  43704  wepwsolem  43802  mendring  43948  mendlmod  43949  hausgraph  43965  cantnftermord  44080  cantnfub  44081  cantnf2  44085  omabs2  44092  rp-isfinite5  44276  omelaxinf2  45731  cncmpmax  45785  eliinid  45862  icccncfext  46634  dvnprodlem2  46694  stoweidlem7  46754  stoweidlem34  46781  stoweidlem35  46782  stoweidlem59  46806  stoweidlem60  46807  stoweidlem62  46809  fourierdlem34  46888  fourierdlem73  46926  fourierdlem77  46930  etransclem35  47016  smfsuplem2  47559  pgrple2abl  49178  clddisj  49715