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  6180  ordin  6388  fimacnvdisj  6753  f1oexrnex  7924  wemoiso  7970  wemoiso2  7971  smocdmdom  8357  rdglim  8415  oaabs  8636  ecref  8742  f1oenfi  9173  f1oenfirn  9174  f1domfi  9175  domfi  9183  sdomdomtrfi  9195  php  9201  f1vrnfibi  9309  brwdom2  9545  infdiffi  9637  cantnflem1  9668  wemapwe  9676  cnfcom3lem  9682  r1lim  9754  carduni  9986  ac5num  10039  infunsdom1  10214  cofsmo  10271  isf32lem6  10360  hsmexlem1  10428  ac6c4  10483  fnct  10544  fnctOLD  10545  pwfseqlem1  10667  tskuni  10792  recgt1i  12136  avgle2  12509  eluzmn  12894  rpnnen1lem1  13028  xnn0le2is012  13298  fzneuz  13663  mulmod0  13938  hasheni  14412  hashun2  14447  hashf1dmrn  14508  reccn2  15684  isershft  15751  sumeq2ii  15780  prodeq2ii  16000  demoivreALT  16289  bitsp1  16521  gcdneg  16612  eucalginv  16674  eucalg  16677  odzdvds  16887  fldivp1  16989  prmunb  17006  vdwap1  17069  setsid  17299  acsmapd  18642  intopsn  18746  cntzidss  19467  symggrp  19527  pmtrfv  19579  odmodnn0  19667  sylow2alem1  19744  telgsumfzs  20116  dprdsn  20165  dvdsrmul1  20510  dvrid  20547  cntzsubrng  20729  prmidl0  21541  znunit  21776  isphld  21867  frlmup1  22011  evl1val  22554  evl1sca  22559  pf1const  22571  mat1f1o  22700  mat1mhm  22706  matunit  22900  matunitlindf  22903  pm2mpmhmlem2  23044  cctop  23231  iscnp4  23488  iscncl  23494  cnntr  23500  tx2cn  23836  xkoco1cn  23883  qtopkgen  23936  hmeontr  23995  hmeores  23997  filssufilg  24137  ustuqtop1  24467  utop2nei  24476  fmucndlem  24516  cfilufg  24518  xmetres2  24587  metres2  24589  metustto  24779  metust  24784  cfilucfil  24785  dscopn  24799  nmoi  24954  iccntr  25048  cphsqrtcl2  25414  cmsss  25579  ivthlem3  25681  sca2rab  25740  ovolicc2lem3  25747  mdegleb  26289  mdegmullem  26303  aalioulem3  26570  ulm2  26621  ulmcn  26635  root1eq1  26992  atanlogsublem  27152  birthdaylem3  27190  logexprlim  27461  dchrisumlem3  27727  f1otrg  29327  ax5seglem1  29385  ax5seglem2  29386  ax5seglem3a  29387  ax5seglem4  29389  ax5seglem9  29394  ax5seg  29395  axbtwnid  29396  axlowdimlem17  29415  axcontlem2  29422  axcontlem4  29424  axcontlem8  29428  cyclnumvtx  30267  rusgrnumwwlks  30445  wwlksext2clwwlk  30527  grpoidinv  30989  imsmetlem  31171  ipasslem1  31312  ip2eqi  31337  hvpncan  31520  pjid  32176  hmopre  32404  eigvalcl  32442  leopnmid  32619  superpos  32835  cvp  32856  rabfodom  32980  xlt2addrd  33230  hashxpe  33278  suppgsumssiun  33512  cyc3genpmlem  33591  lmodslmd  33644  elrgspnlem4  33685  elrgspnsubrunlem2  33688  nsgqusf1olem2  33843  elrspunidl  33856  rsprprmprmidlb  33933  extdgfialglem1  34202  irngnminplynz  34222  constrfiss  34261  locfinreflem  34350  zarcls0  34378  fmcncfil  34441  rge0scvg  34459  esumfsup  34580  esumcvg  34596  insiga  34648  ballotlemirc  35043  signstfvcl  35081  signsvfn  35090  upgracycusgr  35734  subfacp1lem6  35764  satfdmlem  35947  msubff1  36135  fv2ndcnv  36357  ovoliunnfl  38411  voliunnfl  38413  volsupnfl  38414  ftc1anclem5  38446  indexa  38483  sstotbnd3  38526  heiborlem6  38566  rngosn3  38674  atlatmstc  40192  atlatle  40193  glbconN  40250  intnatN  40280  lnnat  40300  atcvrj2b  40305  atexchcvrN  40313  llncvrlpln  40431  lplncvrlvol  40489  lautcvr  40965  trlatn0  41045  cdleme48fvg  41373  cdlemg33c  41581  dihcl  42143  imadomfi  42868  fsuppssind  43439  elpell1qr2  43713  oddcomabszz  43785  wepwsolem  43883  mendring  44029  mendlmod  44030  hausgraph  44046  cantnftermord  44161  cantnfub  44162  cantnf2  44166  omabs2  44173  rp-isfinite5  44357  omelaxinf2  45812  cncmpmax  45866  eliinid  45943  icccncfext  46715  dvnprodlem2  46775  stoweidlem7  46835  stoweidlem34  46862  stoweidlem35  46863  stoweidlem59  46887  stoweidlem60  46888  stoweidlem62  46890  fourierdlem34  46969  fourierdlem73  47007  fourierdlem77  47011  etransclem35  47097  smfsuplem2  47640  pgrple2abl  49295  clddisj  49830  veroquadgsumlem  50816