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  6083  ordin  6289  fimacnvdisj  6644  f1oexrnex  7764  wemoiso  7805  wemoiso2  7806  smorndom  8186  rdglim  8244  oaabs  8465  ssct  8826  f1oenfi  8952  f1oenfirn  8953  f1domfi  8954  domfi  8962  sdomdomtrfi  8974  php  8980  onomeneqOLD  8999  f1vrnfibi  9091  brwdom2  9319  infdiffi  9403  cantnflem1  9434  wemapwe  9442  cnfcom3lem  9448  r1lim  9540  carduni  9749  ac5num  9802  infunsdom1  9979  cofsmo  10035  isf32lem6  10124  hsmexlem1  10192  ac6c4  10247  fnct  10303  pwfseqlem1  10424  tskuni  10549  recgt1i  11882  avgle2  12224  eluzmn  12599  rpnnen1lem1  12728  xnn0le2is012  12990  fzneuz  13347  mulmod0  13607  hasheni  14072  hashun2  14108  reccn2  15316  isershft  15385  sumeq2ii  15415  prodeq2ii  15633  demoivreALT  15920  bitsp1  16148  gcdneg  16239  eucalginv  16299  eucalg  16302  odzdvds  16506  fldivp1  16608  prmunb  16625  vdwap1  16688  setsid  16919  acsmapd  18282  intopsn  18348  cntzidss  18954  symggrp  19018  pmtrfv  19070  odmodnn0  19158  sylow2alem1  19232  telgsumfzs  19600  dprdsn  19649  dvdsrmul1  19905  dvrid  19940  znunit  20781  isphld  20869  frlmup1  21015  evl1val  21505  evl1sca  21510  pf1const  21522  mat1f1o  21637  mat1mhm  21643  matunit  21837  pm2mpmhmlem2  21978  cctop  22166  iscnp4  22424  iscncl  22430  cnntr  22436  tx2cn  22771  xkoco1cn  22818  qtopkgen  22871  hmeontr  22930  hmeores  22932  filssufilg  23072  ustuqtop1  23403  utop2nei  23412  fmucndlem  23453  cfilufg  23455  xmetres2  23524  metres2  23526  metustto  23719  metust  23724  cfilucfil  23725  dscopn  23739  nmoi  23902  iccntr  23994  cphsqrtcl2  24360  cmsss  24525  ivthlem3  24627  sca2rab  24686  ovolicc2lem3  24693  mdegleb  25239  mdegmullem  25253  aalioulem3  25504  ulm2  25554  ulmcn  25568  root1eq1  25918  atanlogsublem  26075  birthdaylem3  26113  logexprlim  26383  dchrisumlem3  26649  f1otrg  27242  ax5seglem1  27306  ax5seglem2  27307  ax5seglem3a  27308  ax5seglem4  27310  ax5seglem9  27315  ax5seg  27316  axbtwnid  27317  axlowdimlem17  27336  axcontlem2  27343  axcontlem4  27345  axcontlem8  27349  rusgrnumwwlks  28347  wwlksext2clwwlk  28429  grpoidinv  28878  imsmetlem  29060  ipasslem1  29201  ip2eqi  29226  hvpncan  29409  pjid  30065  hmopre  30293  eigvalcl  30331  leopnmid  30508  superpos  30724  cvp  30745  rabfodom  30859  xlt2addrd  31089  hashxpe  31135  cyc3genpmlem  31426  lmodslmd  31465  nsgqusf1olem2  31607  elrspunidl  31614  prmidl0  31634  locfinreflem  31798  zarcls0  31826  fmcncfil  31889  rge0scvg  31907  esumfsup  32046  esumcvg  32062  insiga  32113  ballotlemirc  32506  signstfvcl  32560  signsvfn  32569  hashf1dmrn  33083  upgracycusgr  33125  subfacp1lem6  33155  satfdmlem  33338  msubff1  33526  fv2ndcnv  33760  matunitlindf  35783  ovoliunnfl  35827  voliunnfl  35829  volsupnfl  35830  ftc1anclem5  35862  indexa  35899  sstotbnd3  35942  heiborlem6  35982  rngosn3  36090  atlatmstc  37341  atlatle  37342  glbconN  37399  intnatN  37429  lnnat  37449  atcvrj2b  37454  atexchcvrN  37462  llncvrlpln  37580  lplncvrlvol  37638  lautcvr  38114  trlatn0  38194  cdleme48fvg  38522  cdlemg33c  38730  dihcl  39292  fsuppssind  40290  elpell1qr2  40702  oddcomabszz  40774  wepwsolem  40875  mendring  41025  mendlmod  41026  hausgraph  41045  rp-isfinite5  41114  cncmpmax  42556  eliinid  42642  icccncfext  43409  dvnprodlem2  43469  stoweidlem7  43529  stoweidlem34  43556  stoweidlem35  43557  stoweidlem59  43581  stoweidlem60  43582  stoweidlem62  43584  fourierdlem34  43663  fourierdlem73  43701  fourierdlem77  43705  etransclem35  43791  smfsuplem2  44323  pgrple2abl  45679  clddisj  46175