Theorem sylancom 586

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

Syntax hints:   → wi 4   ∧ wa 394

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 395

This theorem is referenced by:  sofld  6188  ordin  6395  fimacnvdisj  6769  f1oexrnex  7929  wemoiso  7976  wemoiso2  7977  smocdmdom  8387  rdglim  8445  oaabs  8667  ecref  8768  ssctOLD  9079  f1oenfi  9206  f1oenfirn  9207  f1domfi  9208  domfi  9216  sdomdomtrfi  9228  php  9234  onomeneqOLD  9253  f1vrnfibi  9374  brwdom2  9606  infdiffi  9691  cantnflem1  9722  wemapwe  9730  cnfcom3lem  9736  r1lim  9805  carduni  10014  ac5num  10069  infunsdom1  10244  cofsmo  10300  isf32lem6  10389  hsmexlem1  10457  ac6c4  10512  fnct  10568  pwfseqlem1  10689  tskuni  10814  recgt1i  12154  avgle2  12496  eluzmn  12872  rpnnen1lem1  13005  xnn0le2is012  13270  fzneuz  13627  mulmod0  13888  hasheni  14357  hashun2  14392  hashf1dmrn  14452  reccn2  15591  isershft  15660  sumeq2ii  15689  prodeq2ii  15907  demoivreALT  16195  bitsp1  16423  gcdneg  16514  eucalginv  16577  eucalg  16580  odzdvds  16789  fldivp1  16891  prmunb  16908  vdwap1  16971  setsid  17202  acsmapd  18571  intopsn  18639  cntzidss  19327  symggrp  19391  pmtrfv  19443  odmodnn0  19531  sylow2alem1  19608  telgsumfzs  19980  dprdsn  20029  dvdsrmul1  20344  dvrid  20381  cntzsubrng  20542  znunit  21554  isphld  21643  frlmup1  21789  evl1val  22314  evl1sca  22319  pf1const  22331  mat1f1o  22465  mat1mhm  22471  matunit  22665  pm2mpmhmlem2  22806  cctop  22994  iscnp4  23252  iscncl  23258  cnntr  23264  tx2cn  23599  xkoco1cn  23646  qtopkgen  23699  hmeontr  23758  hmeores  23760  filssufilg  23900  ustuqtop1  24231  utop2nei  24240  fmucndlem  24281  cfilufg  24283  xmetres2  24352  metres2  24354  metustto  24547  metust  24552  cfilucfil  24553  dscopn  24567  nmoi  24730  iccntr  24822  cphsqrtcl2  25199  cmsss  25364  ivthlem3  25467  sca2rab  25526  ovolicc2lem3  25533  mdegleb  26085  mdegmullem  26099  aalioulem3  26356  ulm2  26408  ulmcn  26422  root1eq1  26777  atanlogsublem  26937  birthdaylem3  26975  logexprlim  27248  dchrisumlem3  27514  f1otrg  28792  ax5seglem1  28856  ax5seglem2  28857  ax5seglem3a  28858  ax5seglem4  28860  ax5seglem9  28865  ax5seg  28866  axbtwnid  28867  axlowdimlem17  28886  axcontlem2  28893  axcontlem4  28895  axcontlem8  28899  rusgrnumwwlks  29902  wwlksext2clwwlk  29984  grpoidinv  30435  imsmetlem  30617  ipasslem1  30758  ip2eqi  30783  hvpncan  30966  pjid  31622  hmopre  31850  eigvalcl  31888  leopnmid  32065  superpos  32281  cvp  32302  rabfodom  32428  xlt2addrd  32662  hashxpe  32711  cyc3genpmlem  33030  lmodslmd  33069  nsgqusf1olem2  33292  elrspunidl  33306  prmidl0  33328  rsprprmprmidlb  33401  irngnminplynz  33584  locfinreflem  33665  zarcls0  33693  fmcncfil  33756  rge0scvg  33774  esumfsup  33913  esumcvg  33929  insiga  33980  ballotlemirc  34375  signstfvcl  34429  signsvfn  34438  upgracycusgr  34993  subfacp1lem6  35023  satfdmlem  35206  msubff1  35394  fv2ndcnv  35611  matunitlindf  37329  ovoliunnfl  37373  voliunnfl  37375  volsupnfl  37376  ftc1anclem5  37408  indexa  37444  sstotbnd3  37487  heiborlem6  37527  rngosn3  37635  atlatmstc  39027  atlatle  39028  glbconN  39085  glbconNOLD  39086  intnatN  39116  lnnat  39136  atcvrj2b  39141  atexchcvrN  39149  llncvrlpln  39267  lplncvrlvol  39325  lautcvr  39801  trlatn0  39881  cdleme48fvg  40209  cdlemg33c  40417  dihcl  40979  imadomfi  41711  fsuppssind  42280  elpell1qr2  42563  oddcomabszz  42636  wepwsolem  42737  mendring  42887  mendlmod  42888  hausgraph  42904  cantnftermord  43020  cantnfub  43021  cantnf2  43025  omabs2  43032  rp-isfinite5  43218  cncmpmax  44665  eliinid  44746  icccncfext  45541  dvnprodlem2  45601  stoweidlem7  45661  stoweidlem34  45688  stoweidlem35  45689  stoweidlem59  45713  stoweidlem60  45714  stoweidlem62  45716  fourierdlem34  45795  fourierdlem73  45833  fourierdlem77  45837  etransclem35  45923  smfsuplem2  46466  pgrple2abl  47777  clddisj  48270