Theorem sylancom 594

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 590	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 208  df-an 397

This theorem is referenced by:  sofld  6138  ordin  6340  fimacnvdisj  6705  f1oexrnex  7867  wemoiso  7915  wemoiso2  7916  smocdmdom  8298  rdglim  8355  oaabs  8574  ecref  8679  f1oenfi  9103  f1oenfirn  9104  f1domfi  9105  domfi  9113  sdomdomtrfi  9125  php  9131  f1vrnfibi  9242  brwdom2  9478  infdiffi  9570  cantnflem1  9601  wemapwe  9609  cnfcom3lem  9615  r1lim  9687  carduni  9896  ac5num  9949  infunsdom1  10125  cofsmo  10182  isf32lem6  10271  hsmexlem1  10339  ac6c4  10394  fnct  10450  pwfseqlem1  10572  tskuni  10697  recgt1i  12044  avgle2  12409  eluzmn  12786  rpnnen1lem1  12919  xnn0le2is012  13189  fzneuz  13553  mulmod0  13827  hasheni  14301  hashun2  14336  hashf1dmrn  14396  reccn2  15550  isershft  15617  sumeq2ii  15646  prodeq2ii  15867  demoivreALT  16159  bitsp1  16391  gcdneg  16482  eucalginv  16544  eucalg  16547  odzdvds  16757  fldivp1  16859  prmunb  16876  vdwap1  16939  setsid  17168  acsmapd  18511  intopsn  18613  cntzidss  19306  symggrp  19366  pmtrfv  19418  odmodnn0  19506  sylow2alem1  19583  telgsumfzs  19955  dprdsn  20004  dvdsrmul1  20340  dvrid  20377  cntzsubrng  20539  znunit  21538  isphld  21629  frlmup1  21773  evl1val  22315  evl1sca  22320  pf1const  22332  mat1f1o  22461  mat1mhm  22467  matunit  22661  pm2mpmhmlem2  22802  cctop  22989  iscnp4  23246  iscncl  23252  cnntr  23258  tx2cn  23593  xkoco1cn  23640  qtopkgen  23693  hmeontr  23752  hmeores  23754  filssufilg  23894  ustuqtop1  24224  utop2nei  24233  fmucndlem  24273  cfilufg  24275  xmetres2  24344  metres2  24346  metustto  24536  metust  24541  cfilucfil  24542  dscopn  24556  nmoi  24711  iccntr  24805  cphsqrtcl2  25171  cmsss  25336  ivthlem3  25438  sca2rab  25497  ovolicc2lem3  25504  mdegleb  26047  mdegmullem  26061  aalioulem3  26318  ulm2  26368  ulmcn  26382  root1eq1  26737  atanlogsublem  26897  birthdaylem3  26935  logexprlim  27206  dchrisumlem3  27472  f1otrg  28957  ax5seglem1  29015  ax5seglem2  29016  ax5seglem3a  29017  ax5seglem4  29019  ax5seglem9  29024  ax5seg  29025  axbtwnid  29026  axlowdimlem17  29045  axcontlem2  29052  axcontlem4  29054  axcontlem8  29058  cyclnumvtx  29886  rusgrnumwwlks  30063  wwlksext2clwwlk  30145  grpoidinv  30597  imsmetlem  30779  ipasslem1  30920  ip2eqi  30945  hvpncan  31128  pjid  31784  hmopre  32012  eigvalcl  32050  leopnmid  32227  superpos  32443  cvp  32464  rabfodom  32593  xlt2addrd  32851  hashxpe  32899  suppgsumssiun  33153  cyc3genpmlem  33232  lmodslmd  33285  elrgspnlem4  33326  elrgspnsubrunlem2  33329  nsgqusf1olem2  33497  elrspunidl  33511  prmidl0  33533  rsprprmprmidlb  33606  extdgfialglem1  33876  irngnminplynz  33896  constrfiss  33935  locfinreflem  34024  zarcls0  34052  fmcncfil  34115  rge0scvg  34133  esumfsup  34254  esumcvg  34270  insiga  34321  ballotlemirc  34716  signstfvcl  34757  signsvfn  34766  upgracycusgr  35383  subfacp1lem6  35413  satfdmlem  35596  msubff1  35784  fv2ndcnv  36006  matunitlindf  37985  ovoliunnfl  38029  voliunnfl  38031  volsupnfl  38032  ftc1anclem5  38064  indexa  38100  sstotbnd3  38143  heiborlem6  38183  rngosn3  38291  atlatmstc  39811  atlatle  39812  glbconN  39869  intnatN  39899  lnnat  39919  atcvrj2b  39924  atexchcvrN  39932  llncvrlpln  40050  lplncvrlvol  40108  lautcvr  40584  trlatn0  40664  cdleme48fvg  40992  cdlemg33c  41200  dihcl  41762  imadomfi  42487  fsuppssind  43043  elpell1qr2  43317  oddcomabszz  43389  wepwsolem  43487  mendring  43633  mendlmod  43634  hausgraph  43650  cantnftermord  43765  cantnfub  43766  cantnf2  43770  omabs2  43777  rp-isfinite5  43961  omelaxinf2  45433  cncmpmax  45480  eliinid  45558  icccncfext  46330  dvnprodlem2  46390  stoweidlem7  46450  stoweidlem34  46477  stoweidlem35  46478  stoweidlem59  46502  stoweidlem60  46503  stoweidlem62  46505  fourierdlem34  46584  fourierdlem73  46622  fourierdlem77  46626  etransclem35  46712  smfsuplem2  47255  pgrple2abl  48856  clddisj  49394