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

Syntax hints:   → wi 4   ∧ wa 396

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 206  df-an 397

This theorem is referenced by:  sofld  6095  ordin  6300  fimacnvdisj  6661  f1oexrnex  7783  wemoiso  7825  wemoiso2  7826  smorndom  8208  rdglim  8266  oaabs  8487  ssct  8848  f1oenfi  8974  f1oenfirn  8975  f1domfi  8976  domfi  8984  sdomdomtrfi  8996  php  9002  onomeneqOLD  9021  f1vrnfibi  9113  brwdom2  9341  infdiffi  9425  cantnflem1  9456  wemapwe  9464  cnfcom3lem  9470  r1lim  9539  carduni  9748  ac5num  9801  infunsdom1  9978  cofsmo  10034  isf32lem6  10123  hsmexlem1  10191  ac6c4  10246  fnct  10302  pwfseqlem1  10423  tskuni  10548  recgt1i  11881  avgle2  12223  eluzmn  12598  rpnnen1lem1  12727  xnn0le2is012  12989  fzneuz  13346  mulmod0  13606  hasheni  14071  hashun2  14107  reccn2  15315  isershft  15384  sumeq2ii  15414  prodeq2ii  15632  demoivreALT  15919  bitsp1  16147  gcdneg  16238  eucalginv  16298  eucalg  16301  odzdvds  16505  fldivp1  16607  prmunb  16624  vdwap1  16687  setsid  16918  acsmapd  18281  intopsn  18347  cntzidss  18953  symggrp  19017  pmtrfv  19069  odmodnn0  19157  sylow2alem1  19231  telgsumfzs  19599  dprdsn  19648  dvdsrmul1  19904  dvrid  19939  znunit  20780  isphld  20868  frlmup1  21014  evl1val  21504  evl1sca  21509  pf1const  21521  mat1f1o  21636  mat1mhm  21642  matunit  21836  pm2mpmhmlem2  21977  cctop  22165  iscnp4  22423  iscncl  22429  cnntr  22435  tx2cn  22770  xkoco1cn  22817  qtopkgen  22870  hmeontr  22929  hmeores  22931  filssufilg  23071  ustuqtop1  23402  utop2nei  23411  fmucndlem  23452  cfilufg  23454  xmetres2  23523  metres2  23525  metustto  23718  metust  23723  cfilucfil  23724  dscopn  23738  nmoi  23901  iccntr  23993  cphsqrtcl2  24359  cmsss  24524  ivthlem3  24626  sca2rab  24685  ovolicc2lem3  24692  mdegleb  25238  mdegmullem  25252  aalioulem3  25503  ulm2  25553  ulmcn  25567  root1eq1  25917  atanlogsublem  26074  birthdaylem3  26112  logexprlim  26382  dchrisumlem3  26648  f1otrg  27241  ax5seglem1  27305  ax5seglem2  27306  ax5seglem3a  27307  ax5seglem4  27309  ax5seglem9  27314  ax5seg  27315  axbtwnid  27316  axlowdimlem17  27335  axcontlem2  27342  axcontlem4  27344  axcontlem8  27348  rusgrnumwwlks  28348  wwlksext2clwwlk  28430  grpoidinv  28879  imsmetlem  29061  ipasslem1  29202  ip2eqi  29227  hvpncan  29410  pjid  30066  hmopre  30294  eigvalcl  30332  leopnmid  30509  superpos  30725  cvp  30746  rabfodom  30860  xlt2addrd  31090  hashxpe  31136  cyc3genpmlem  31427  lmodslmd  31466  nsgqusf1olem2  31608  elrspunidl  31615  prmidl0  31635  locfinreflem  31799  zarcls0  31827  fmcncfil  31890  rge0scvg  31908  esumfsup  32047  esumcvg  32063  insiga  32114  ballotlemirc  32507  signstfvcl  32561  signsvfn  32570  hashf1dmrn  33084  upgracycusgr  33126  subfacp1lem6  33156  satfdmlem  33339  msubff1  33527  fv2ndcnv  33761  matunitlindf  35784  ovoliunnfl  35828  voliunnfl  35830  volsupnfl  35831  ftc1anclem5  35863  indexa  35900  sstotbnd3  35943  heiborlem6  35983  rngosn3  36091  atlatmstc  37340  atlatle  37341  glbconN  37398  intnatN  37428  lnnat  37448  atcvrj2b  37453  atexchcvrN  37461  llncvrlpln  37579  lplncvrlvol  37637  lautcvr  38113  trlatn0  38193  cdleme48fvg  38521  cdlemg33c  38729  dihcl  39291  fsuppssind  40289  elpell1qr2  40701  oddcomabszz  40773  wepwsolem  40874  mendring  41024  mendlmod  41025  hausgraph  41044  rp-isfinite5  41131  cncmpmax  42582  eliinid  42668  icccncfext  43435  dvnprodlem2  43495  stoweidlem7  43555  stoweidlem34  43582  stoweidlem35  43583  stoweidlem59  43607  stoweidlem60  43608  stoweidlem62  43610  fourierdlem34  43689  fourierdlem73  43727  fourierdlem77  43731  etransclem35  43817  smfsuplem2  44356  pgrple2abl  45712  clddisj  46208