Theorem sylancom 597

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

Syntax hints:   → wi 4   ∧ wa 399

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 209  df-an 400

This theorem is referenced by:  sofld  6168  ordin  6371  fimacnvdisj  6737  f1oexrnex  7903  wemoiso  7949  wemoiso2  7950  smocdmdom  8333  rdglim  8391  oaabs  8612  ecref  8718  f1oenfi  9141  f1oenfirn  9142  f1domfi  9143  domfi  9151  sdomdomtrfi  9163  php  9169  f1vrnfibi  9279  brwdom2  9515  infdiffi  9607  cantnflem1  9638  wemapwe  9646  cnfcom3lem  9652  r1lim  9724  carduni  9933  ac5num  9986  infunsdom1  10162  cofsmo  10220  isf32lem6  10309  hsmexlem1  10377  ac6c4  10432  fnct  10488  pwfseqlem1  10610  tskuni  10735  recgt1i  12083  avgle2  12456  eluzmn  12840  rpnnen1lem1  12973  xnn0le2is012  13243  fzneuz  13607  mulmod0  13881  hasheni  14355  hashun2  14390  hashf1dmrn  14450  reccn2  15615  isershft  15682  sumeq2ii  15711  prodeq2ii  15932  demoivreALT  16224  bitsp1  16456  gcdneg  16547  eucalginv  16609  eucalg  16612  odzdvds  16822  fldivp1  16924  prmunb  16941  vdwap1  17004  setsid  17234  acsmapd  18577  intopsn  18679  cntzidss  19371  symggrp  19431  pmtrfv  19483  odmodnn0  19571  sylow2alem1  19648  telgsumfzs  20020  dprdsn  20069  dvdsrmul1  20405  dvrid  20442  cntzsubrng  20604  znunit  21603  isphld  21694  frlmup1  21838  evl1val  22380  evl1sca  22385  pf1const  22397  mat1f1o  22526  mat1mhm  22532  matunit  22726  pm2mpmhmlem2  22867  cctop  23054  iscnp4  23311  iscncl  23317  cnntr  23323  tx2cn  23658  xkoco1cn  23705  qtopkgen  23758  hmeontr  23817  hmeores  23819  filssufilg  23959  ustuqtop1  24289  utop2nei  24298  fmucndlem  24338  cfilufg  24340  xmetres2  24409  metres2  24411  metustto  24601  metust  24606  cfilucfil  24607  dscopn  24621  nmoi  24776  iccntr  24870  cphsqrtcl2  25236  cmsss  25401  ivthlem3  25503  sca2rab  25562  ovolicc2lem3  25569  mdegleb  26112  mdegmullem  26126  aalioulem3  26386  ulm2  26436  ulmcn  26450  root1eq1  26808  atanlogsublem  26968  birthdaylem3  27006  logexprlim  27277  dchrisumlem3  27543  f1otrg  29028  ax5seglem1  29086  ax5seglem2  29087  ax5seglem3a  29088  ax5seglem4  29090  ax5seglem9  29095  ax5seg  29096  axbtwnid  29097  axlowdimlem17  29116  axcontlem2  29123  axcontlem4  29125  axcontlem8  29129  cyclnumvtx  29957  rusgrnumwwlks  30134  wwlksext2clwwlk  30216  grpoidinv  30668  imsmetlem  30850  ipasslem1  30991  ip2eqi  31016  hvpncan  31199  pjid  31855  hmopre  32083  eigvalcl  32121  leopnmid  32298  superpos  32514  cvp  32535  rabfodom  32664  xlt2addrd  32922  hashxpe  32970  suppgsumssiun  33213  cyc3genpmlem  33292  lmodslmd  33345  elrgspnlem4  33387  elrgspnsubrunlem2  33390  nsgqusf1olem2  33561  elrspunidl  33575  prmidl0  33598  rsprprmprmidlb  33680  extdgfialglem1  33950  irngnminplynz  33970  constrfiss  34009  locfinreflem  34098  zarcls0  34126  fmcncfil  34189  rge0scvg  34207  esumfsup  34328  esumcvg  34344  insiga  34395  ballotlemirc  34790  signstfvcl  34828  signsvfn  34837  upgracycusgr  35466  subfacp1lem6  35496  satfdmlem  35679  msubff1  35867  fv2ndcnv  36089  matunitlindf  38078  ovoliunnfl  38122  voliunnfl  38124  volsupnfl  38125  ftc1anclem5  38157  indexa  38193  sstotbnd3  38236  heiborlem6  38276  rngosn3  38384  atlatmstc  39904  atlatle  39905  glbconN  39962  intnatN  39992  lnnat  40012  atcvrj2b  40017  atexchcvrN  40025  llncvrlpln  40143  lplncvrlvol  40201  lautcvr  40677  trlatn0  40757  cdleme48fvg  41085  cdlemg33c  41293  dihcl  41855  imadomfi  42580  fsuppssind  43136  elpell1qr2  43410  oddcomabszz  43482  wepwsolem  43580  mendring  43726  mendlmod  43727  hausgraph  43743  cantnftermord  43858  cantnfub  43859  cantnf2  43863  omabs2  43870  rp-isfinite5  44054  omelaxinf2  45526  cncmpmax  45573  eliinid  45650  icccncfext  46422  dvnprodlem2  46482  stoweidlem7  46542  stoweidlem34  46569  stoweidlem35  46570  stoweidlem59  46594  stoweidlem60  46595  stoweidlem62  46597  fourierdlem34  46676  fourierdlem73  46714  fourierdlem77  46718  etransclem35  46804  smfsuplem2  47347  pgrple2abl  48948  clddisj  49486