Theorem sylancom 589

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 585	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  6153  ordin  6355  fimacnvdisj  6720  f1oexrnex  7879  wemoiso  7927  wemoiso2  7928  smocdmdom  8310  rdglim  8367  oaabs  8586  ecref  8691  f1oenfi  9115  f1oenfirn  9116  f1domfi  9117  domfi  9125  sdomdomtrfi  9137  php  9143  f1vrnfibi  9254  brwdom2  9490  infdiffi  9579  cantnflem1  9610  wemapwe  9618  cnfcom3lem  9624  r1lim  9696  carduni  9905  ac5num  9958  infunsdom1  10134  cofsmo  10191  isf32lem6  10280  hsmexlem1  10348  ac6c4  10403  fnct  10459  pwfseqlem1  10581  tskuni  10706  recgt1i  12051  avgle2  12394  eluzmn  12770  rpnnen1lem1  12903  xnn0le2is012  13173  fzneuz  13536  mulmod0  13809  hasheni  14283  hashun2  14318  hashf1dmrn  14378  reccn2  15532  isershft  15599  sumeq2ii  15628  prodeq2ii  15846  demoivreALT  16138  bitsp1  16370  gcdneg  16461  eucalginv  16523  eucalg  16526  odzdvds  16735  fldivp1  16837  prmunb  16854  vdwap1  16917  setsid  17146  acsmapd  18489  intopsn  18591  cntzidss  19281  symggrp  19341  pmtrfv  19393  odmodnn0  19481  sylow2alem1  19558  telgsumfzs  19930  dprdsn  19979  dvdsrmul1  20317  dvrid  20354  cntzsubrng  20512  znunit  21530  isphld  21621  frlmup1  21765  evl1val  22285  evl1sca  22290  pf1const  22302  mat1f1o  22434  mat1mhm  22440  matunit  22634  pm2mpmhmlem2  22775  cctop  22962  iscnp4  23219  iscncl  23225  cnntr  23231  tx2cn  23566  xkoco1cn  23613  qtopkgen  23666  hmeontr  23725  hmeores  23727  filssufilg  23867  ustuqtop1  24197  utop2nei  24206  fmucndlem  24246  cfilufg  24248  xmetres2  24317  metres2  24319  metustto  24509  metust  24514  cfilucfil  24515  dscopn  24529  nmoi  24684  iccntr  24778  cphsqrtcl2  25154  cmsss  25319  ivthlem3  25422  sca2rab  25481  ovolicc2lem3  25488  mdegleb  26037  mdegmullem  26051  aalioulem3  26310  ulm2  26362  ulmcn  26376  root1eq1  26733  atanlogsublem  26893  birthdaylem3  26931  logexprlim  27204  dchrisumlem3  27470  f1otrg  28955  ax5seglem1  29013  ax5seglem2  29014  ax5seglem3a  29015  ax5seglem4  29017  ax5seglem9  29022  ax5seg  29023  axbtwnid  29024  axlowdimlem17  29043  axcontlem2  29050  axcontlem4  29052  axcontlem8  29056  cyclnumvtx  29885  rusgrnumwwlks  30062  wwlksext2clwwlk  30144  grpoidinv  30595  imsmetlem  30777  ipasslem1  30918  ip2eqi  30943  hvpncan  31126  pjid  31782  hmopre  32010  eigvalcl  32048  leopnmid  32225  superpos  32441  cvp  32462  rabfodom  32591  xlt2addrd  32849  hashxpe  32897  suppgsumssiun  33165  cyc3genpmlem  33244  lmodslmd  33297  elrgspnlem4  33338  elrgspnsubrunlem2  33341  nsgqusf1olem2  33506  elrspunidl  33520  prmidl0  33542  rsprprmprmidlb  33615  extdgfialglem1  33869  irngnminplynz  33889  constrfiss  33928  locfinreflem  34017  zarcls0  34045  fmcncfil  34108  rge0scvg  34126  esumfsup  34247  esumcvg  34263  insiga  34314  ballotlemirc  34709  signstfvcl  34750  signsvfn  34759  upgracycusgr  35368  subfacp1lem6  35398  satfdmlem  35581  msubff1  35769  fv2ndcnv  35991  matunitlindf  37866  ovoliunnfl  37910  voliunnfl  37912  volsupnfl  37913  ftc1anclem5  37945  indexa  37981  sstotbnd3  38024  heiborlem6  38064  rngosn3  38172  atlatmstc  39692  atlatle  39693  glbconN  39750  intnatN  39780  lnnat  39800  atcvrj2b  39805  atexchcvrN  39813  llncvrlpln  39931  lplncvrlvol  39989  lautcvr  40465  trlatn0  40545  cdleme48fvg  40873  cdlemg33c  41081  dihcl  41643  imadomfi  42369  fsuppssind  42948  elpell1qr2  43226  oddcomabszz  43298  wepwsolem  43396  mendring  43542  mendlmod  43543  hausgraph  43559  cantnftermord  43674  cantnfub  43675  cantnf2  43679  omabs2  43686  rp-isfinite5  43870  omelaxinf2  45342  cncmpmax  45389  eliinid  45467  icccncfext  46242  dvnprodlem2  46302  stoweidlem7  46362  stoweidlem34  46389  stoweidlem35  46390  stoweidlem59  46414  stoweidlem60  46415  stoweidlem62  46417  fourierdlem34  46496  fourierdlem73  46534  fourierdlem77  46538  etransclem35  46624  smfsuplem2  47167  pgrple2abl  48722  clddisj  49260