Theorem sylancom 588

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

Syntax hints:   → wi 4   ∧ wa 395

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 207  df-an 396

This theorem is referenced by:  sofld  6148  ordin  6350  fimacnvdisj  6720  f1oexrnex  7883  wemoiso  7931  wemoiso2  7932  smocdmdom  8314  rdglim  8371  oaabs  8589  ecref  8693  f1oenfi  9120  f1oenfirn  9121  f1domfi  9122  domfi  9130  sdomdomtrfi  9142  php  9148  f1vrnfibi  9269  brwdom2  9502  infdiffi  9587  cantnflem1  9618  wemapwe  9626  cnfcom3lem  9632  r1lim  9701  carduni  9910  ac5num  9965  infunsdom1  10141  cofsmo  10198  isf32lem6  10287  hsmexlem1  10355  ac6c4  10410  fnct  10466  pwfseqlem1  10587  tskuni  10712  recgt1i  12056  avgle2  12399  eluzmn  12776  rpnnen1lem1  12913  xnn0le2is012  13182  fzneuz  13545  mulmod0  13815  hasheni  14289  hashun2  14324  hashf1dmrn  14384  reccn2  15539  isershft  15606  sumeq2ii  15635  prodeq2ii  15853  demoivreALT  16145  bitsp1  16377  gcdneg  16468  eucalginv  16530  eucalg  16533  odzdvds  16742  fldivp1  16844  prmunb  16861  vdwap1  16924  setsid  17153  acsmapd  18489  intopsn  18557  cntzidss  19248  symggrp  19306  pmtrfv  19358  odmodnn0  19446  sylow2alem1  19523  telgsumfzs  19895  dprdsn  19944  dvdsrmul1  20254  dvrid  20291  cntzsubrng  20452  znunit  21449  isphld  21539  frlmup1  21683  evl1val  22192  evl1sca  22197  pf1const  22209  mat1f1o  22341  mat1mhm  22347  matunit  22541  pm2mpmhmlem2  22682  cctop  22869  iscnp4  23126  iscncl  23132  cnntr  23138  tx2cn  23473  xkoco1cn  23520  qtopkgen  23573  hmeontr  23632  hmeores  23634  filssufilg  23774  ustuqtop1  24105  utop2nei  24114  fmucndlem  24154  cfilufg  24156  xmetres2  24225  metres2  24227  metustto  24417  metust  24422  cfilucfil  24423  dscopn  24437  nmoi  24592  iccntr  24686  cphsqrtcl2  25062  cmsss  25227  ivthlem3  25330  sca2rab  25389  ovolicc2lem3  25396  mdegleb  25945  mdegmullem  25959  aalioulem3  26218  ulm2  26270  ulmcn  26284  root1eq1  26641  atanlogsublem  26801  birthdaylem3  26839  logexprlim  27112  dchrisumlem3  27378  f1otrg  28774  ax5seglem1  28831  ax5seglem2  28832  ax5seglem3a  28833  ax5seglem4  28835  ax5seglem9  28840  ax5seg  28841  axbtwnid  28842  axlowdimlem17  28861  axcontlem2  28868  axcontlem4  28870  axcontlem8  28874  cyclnumvtx  29703  rusgrnumwwlks  29877  wwlksext2clwwlk  29959  grpoidinv  30410  imsmetlem  30592  ipasslem1  30733  ip2eqi  30758  hvpncan  30941  pjid  31597  hmopre  31825  eigvalcl  31863  leopnmid  32040  superpos  32256  cvp  32277  rabfodom  32407  xlt2addrd  32655  hashxpe  32705  cyc3genpmlem  33081  lmodslmd  33130  elrgspnlem4  33169  elrgspnsubrunlem2  33172  nsgqusf1olem2  33358  elrspunidl  33372  prmidl0  33394  rsprprmprmidlb  33467  irngnminplynz  33675  constrfiss  33714  locfinreflem  33803  zarcls0  33831  fmcncfil  33894  rge0scvg  33912  esumfsup  34033  esumcvg  34049  insiga  34100  ballotlemirc  34496  signstfvcl  34537  signsvfn  34546  upgracycusgr  35115  subfacp1lem6  35145  satfdmlem  35328  msubff1  35516  fv2ndcnv  35738  matunitlindf  37585  ovoliunnfl  37629  voliunnfl  37631  volsupnfl  37632  ftc1anclem5  37664  indexa  37700  sstotbnd3  37743  heiborlem6  37783  rngosn3  37891  atlatmstc  39285  atlatle  39286  glbconN  39343  glbconNOLD  39344  intnatN  39374  lnnat  39394  atcvrj2b  39399  atexchcvrN  39407  llncvrlpln  39525  lplncvrlvol  39583  lautcvr  40059  trlatn0  40139  cdleme48fvg  40467  cdlemg33c  40675  dihcl  41237  imadomfi  41963  fsuppssind  42554  elpell1qr2  42833  oddcomabszz  42906  wepwsolem  43004  mendring  43150  mendlmod  43151  hausgraph  43167  cantnftermord  43282  cantnfub  43283  cantnf2  43287  omabs2  43294  rp-isfinite5  43479  omelaxinf2  44952  cncmpmax  44999  eliinid  45078  icccncfext  45858  dvnprodlem2  45918  stoweidlem7  45978  stoweidlem34  46005  stoweidlem35  46006  stoweidlem59  46030  stoweidlem60  46031  stoweidlem62  46033  fourierdlem34  46112  fourierdlem73  46150  fourierdlem77  46154  etransclem35  46240  smfsuplem2  46783  pgrple2abl  48326  clddisj  48865