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  6179  ordin  6392  fimacnvdisj  6758  f1oexrnex  7937  wemoiso  7983  wemoiso2  7984  smocdmdom  8369  rdglim  8427  oaabs  8650  ecref  8756  f1oenfi  9187  f1oenfirn  9188  f1domfi  9189  domfi  9197  sdomdomtrfi  9209  php  9215  f1vrnfibi  9324  brwdom2  9560  infdiffi  9652  cantnflem1  9683  wemapwe  9691  cnfcom3lem  9697  r1lim  9772  carduni  10055  ac5num  10108  infunsdom1  10283  cofsmo  10340  isf32lem6  10429  hsmexlem1  10497  ac6c4  10552  fnct  10613  fnctOLD  10614  pwfseqlem1  10736  tskuni  10861  recgt1i  12207  avgle2  12580  eluzmn  12965  rpnnen1lem1  13099  xnn0le2is012  13369  fzneuz  13735  mulmod0  14010  hasheni  14485  hashun2  14520  hashf1dmrn  14581  reccn2  15757  isershft  15824  sumeq2ii  15853  prodeq2ii  16073  demoivreALT  16362  bitsp1  16594  gcdneg  16687  eucalginv  16752  eucalg  16755  odzdvds  16966  fldivp1  17068  prmunb  17085  vdwap1  17148  setsid  17378  acsmapd  18721  intopsn  18825  cntzidss  19547  symggrp  19607  pmtrfv  19659  odmodnn0  19747  sylow2alem1  19824  telgsumfzs  20196  dprdsn  20245  dvdsrmul1  20592  dvrid  20629  cntzsubrng  20812  prmidl0  21627  znunit  21862  isphld  21953  frlmup1  22097  evl1val  22640  evl1sca  22645  pf1const  22657  mat1f1o  22786  mat1mhm  22792  matunit  22986  matunitlindf  22989  pm2mpmhmlem2  23130  cctop  23317  iscnp4  23574  iscncl  23580  cnntr  23586  tx2cn  23922  xkoco1cn  23969  qtopkgen  24022  hmeontr  24081  hmeores  24083  filssufilg  24223  ustuqtop1  24553  utop2nei  24562  fmucndlem  24602  cfilufg  24604  xmetres2  24673  metres2  24675  metustto  24865  metust  24870  cfilucfil  24871  dscopn  24885  nmoi  25040  iccntr  25134  cphsqrtcl2  25500  cmsss  25665  ivthlem3  25767  sca2rab  25826  ovolicc2lem3  25833  mdegleb  26375  mdegmullem  26389  aalioulem3  26654  ulm2  26705  ulmcn  26719  root1eq1  27076  atanlogsublem  27236  birthdaylem3  27274  logexprlim  27545  dchrisumlem3  27811  f1otrg  29441  ax5seglem1  29499  ax5seglem2  29500  ax5seglem3a  29501  ax5seglem4  29503  ax5seglem9  29508  ax5seg  29509  axbtwnid  29510  axlowdimlem17  29529  axcontlem2  29536  axcontlem4  29538  axcontlem8  29542  cyclnumvtx  30381  rusgrnumwwlks  30559  wwlksext2clwwlk  30641  grpoidinv  31103  imsmetlem  31285  ipasslem1  31426  ip2eqi  31451  hvpncan  31634  pjid  32290  hmopre  32518  eigvalcl  32556  leopnmid  32733  superpos  32949  cvp  32970  rabfodom  33094  xlt2addrd  33344  hashxpe  33392  suppgsumssiun  33626  cyc3genpmlem  33705  lmodslmd  33758  elrgspnlem4  33799  elrgspnsubrunlem2  33802  nsgqusf1olem2  33958  elrspunidl  33971  rsprprmprmidlb  34048  extdgfialglem1  34317  irngnminplynz  34337  constrfiss  34376  locfinreflem  34465  zarcls0  34493  fmcncfil  34556  rge0scvg  34574  esumfsup  34695  esumcvg  34711  insiga  34763  ballotlemirc  35157  signstfvcl  35195  signsvfn  35204  upgracycusgr  35899  subfacp1lem6  35929  satfdmlem  36112  msubff1  36300  fv2ndcnv  36522  ovoliunnfl  38560  voliunnfl  38562  volsupnfl  38563  ftc1anclem5  38595  indexa  38647  sstotbnd3  38690  heiborlem6  38730  rngosn3  38838  atlatmstc  40356  atlatle  40357  glbconN  40414  intnatN  40444  lnnat  40464  atcvrj2b  40469  atexchcvrN  40477  llncvrlpln  40595  lplncvrlvol  40653  lautcvr  41129  trlatn0  41209  cdleme48fvg  41537  cdlemg33c  41745  dihcl  42307  imadomfi  43032  fsuppssind  43601  elpell1qr2  43858  oddcomabszz  43930  wepwsolem  44028  mendring  44174  mendlmod  44175  hausgraph  44191  cantnftermord  44306  cantnfub  44307  cantnf2  44311  omabs2  44318  rp-isfinite5  44502  omelaxinf2  45957  cncmpmax  46018  eliinid  46095  icccncfext  46866  dvnprodlem2  46926  stoweidlem7  46986  stoweidlem34  47013  stoweidlem35  47014  stoweidlem59  47038  stoweidlem60  47039  stoweidlem62  47041  fourierdlem34  47120  fourierdlem73  47158  fourierdlem77  47162  etransclem35  47248  smfsuplem2  47791  pgrple2abl  49446  clddisj  49981  veroquadgsumlem  50952