Theorem sylancom 587

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 583	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 206  df-an 396

This theorem is referenced by:  sofld  6079  ordin  6281  fimacnvdisj  6636  f1oexrnex  7748  wemoiso  7789  wemoiso2  7790  smorndom  8170  rdglim  8228  oaabs  8438  ssct  8793  f1oenfi  8926  f1oenfirn  8927  f1domfi  8928  domfi  8935  onomeneq  8943  f1vrnfibi  9034  brwdom2  9262  infdiffi  9346  cantnflem1  9377  wemapwe  9385  cnfcom3lem  9391  r1lim  9461  carduni  9670  ac5num  9723  infunsdom1  9900  cofsmo  9956  isf32lem6  10045  hsmexlem1  10113  ac6c4  10168  fnct  10224  pwfseqlem1  10345  tskuni  10470  recgt1i  11802  avgle2  12144  eluzmn  12518  rpnnen1lem1  12647  xnn0le2is012  12909  fzneuz  13266  mulmod0  13525  hasheni  13990  hashun2  14026  reccn2  15234  isershft  15303  sumeq2ii  15333  prodeq2ii  15551  demoivreALT  15838  bitsp1  16066  gcdneg  16157  eucalginv  16217  eucalg  16220  odzdvds  16424  fldivp1  16526  prmunb  16543  vdwap1  16606  setsid  16837  acsmapd  18187  intopsn  18253  cntzidss  18859  symggrp  18923  pmtrfv  18975  odmodnn0  19063  sylow2alem1  19137  telgsumfzs  19505  dprdsn  19554  dvdsrmul1  19810  dvrid  19845  znunit  20683  isphld  20771  frlmup1  20915  evl1val  21405  evl1sca  21410  pf1const  21422  mat1f1o  21535  mat1mhm  21541  matunit  21735  pm2mpmhmlem2  21876  cctop  22064  iscnp4  22322  iscncl  22328  cnntr  22334  tx2cn  22669  xkoco1cn  22716  qtopkgen  22769  hmeontr  22828  hmeores  22830  filssufilg  22970  ustuqtop1  23301  utop2nei  23310  fmucndlem  23351  cfilufg  23353  xmetres2  23422  metres2  23424  metustto  23615  metust  23620  cfilucfil  23621  dscopn  23635  nmoi  23798  iccntr  23890  cphsqrtcl2  24255  cmsss  24420  ivthlem3  24522  sca2rab  24581  ovolicc2lem3  24588  mdegleb  25134  mdegmullem  25148  aalioulem3  25399  ulm2  25449  ulmcn  25463  root1eq1  25813  atanlogsublem  25970  birthdaylem3  26008  logexprlim  26278  dchrisumlem3  26544  f1otrg  27136  ax5seglem1  27199  ax5seglem2  27200  ax5seglem3a  27201  ax5seglem4  27203  ax5seglem9  27208  ax5seg  27209  axbtwnid  27210  axlowdimlem17  27229  axcontlem2  27236  axcontlem4  27238  axcontlem8  27242  rusgrnumwwlks  28240  wwlksext2clwwlk  28322  grpoidinv  28771  imsmetlem  28953  ipasslem1  29094  ip2eqi  29119  hvpncan  29302  pjid  29958  hmopre  30186  eigvalcl  30224  leopnmid  30401  superpos  30617  cvp  30638  rabfodom  30752  xlt2addrd  30983  hashxpe  31029  cyc3genpmlem  31320  lmodslmd  31359  nsgqusf1olem2  31501  elrspunidl  31508  prmidl0  31528  locfinreflem  31692  zarcls0  31720  fmcncfil  31783  rge0scvg  31801  esumfsup  31938  esumcvg  31954  insiga  32005  ballotlemirc  32398  signstfvcl  32452  signsvfn  32461  hashf1dmrn  32975  upgracycusgr  33017  subfacp1lem6  33047  satfdmlem  33230  msubff1  33418  fv2ndcnv  33658  matunitlindf  35702  ovoliunnfl  35746  voliunnfl  35748  volsupnfl  35749  ftc1anclem5  35781  indexa  35818  sstotbnd3  35861  heiborlem6  35901  rngosn3  36009  atlatmstc  37260  atlatle  37261  glbconN  37318  intnatN  37348  lnnat  37368  atcvrj2b  37373  atexchcvrN  37381  llncvrlpln  37499  lplncvrlvol  37557  lautcvr  38033  trlatn0  38113  cdleme48fvg  38441  cdlemg33c  38649  dihcl  39211  fsuppssind  40205  elpell1qr2  40610  oddcomabszz  40682  wepwsolem  40783  mendring  40933  mendlmod  40934  hausgraph  40953  rp-isfinite5  41022  cncmpmax  42464  eliinid  42550  icccncfext  43318  dvnprodlem2  43378  stoweidlem7  43438  stoweidlem34  43465  stoweidlem35  43466  stoweidlem59  43490  stoweidlem60  43491  stoweidlem62  43493  fourierdlem34  43572  fourierdlem73  43610  fourierdlem77  43614  etransclem35  43700  smfsuplem2  44232  pgrple2abl  45589  clddisj  46085