Theorem sylancom 589

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 585	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 207  df-an 396

This theorem is referenced by:  sofld  6145  ordin  6347  fimacnvdisj  6712  f1oexrnex  7871  wemoiso  7919  wemoiso2  7920  smocdmdom  8301  rdglim  8358  oaabs  8577  ecref  8682  f1oenfi  9106  f1oenfirn  9107  f1domfi  9108  domfi  9116  sdomdomtrfi  9128  php  9134  f1vrnfibi  9245  brwdom2  9481  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  20535  znunit  21553  isphld  21644  frlmup1  21788  evl1val  22304  evl1sca  22309  pf1const  22321  mat1f1o  22453  mat1mhm  22459  matunit  22653  pm2mpmhmlem2  22794  cctop  22981  iscnp4  23238  iscncl  23244  cnntr  23250  tx2cn  23585  xkoco1cn  23632  qtopkgen  23685  hmeontr  23744  hmeores  23746  filssufilg  23886  ustuqtop1  24216  utop2nei  24225  fmucndlem  24265  cfilufg  24267  xmetres2  24336  metres2  24338  metustto  24528  metust  24533  cfilucfil  24534  dscopn  24548  nmoi  24703  iccntr  24797  cphsqrtcl2  25163  cmsss  25328  ivthlem3  25430  sca2rab  25489  ovolicc2lem3  25496  mdegleb  26039  mdegmullem  26053  aalioulem3  26311  ulm2  26363  ulmcn  26377  root1eq1  26732  atanlogsublem  26892  birthdaylem3  26930  logexprlim  27202  dchrisumlem3  27468  f1otrg  28953  ax5seglem1  29011  ax5seglem2  29012  ax5seglem3a  29013  ax5seglem4  29015  ax5seglem9  29020  ax5seg  29021  axbtwnid  29022  axlowdimlem17  29041  axcontlem2  29048  axcontlem4  29050  axcontlem8  29054  cyclnumvtx  29883  rusgrnumwwlks  30060  wwlksext2clwwlk  30142  grpoidinv  30594  imsmetlem  30776  ipasslem1  30917  ip2eqi  30942  hvpncan  31125  pjid  31781  hmopre  32009  eigvalcl  32047  leopnmid  32224  superpos  32440  cvp  32461  rabfodom  32590  xlt2addrd  32847  hashxpe  32895  suppgsumssiun  33148  cyc3genpmlem  33227  lmodslmd  33280  elrgspnlem4  33321  elrgspnsubrunlem2  33324  nsgqusf1olem2  33489  elrspunidl  33503  prmidl0  33525  rsprprmprmidlb  33598  extdgfialglem1  33852  irngnminplynz  33872  constrfiss  33911  locfinreflem  34000  zarcls0  34028  fmcncfil  34091  rge0scvg  34109  esumfsup  34230  esumcvg  34246  insiga  34297  ballotlemirc  34692  signstfvcl  34733  signsvfn  34742  upgracycusgr  35353  subfacp1lem6  35383  satfdmlem  35566  msubff1  35754  fv2ndcnv  35976  matunitlindf  37953  ovoliunnfl  37997  voliunnfl  37999  volsupnfl  38000  ftc1anclem5  38032  indexa  38068  sstotbnd3  38111  heiborlem6  38151  rngosn3  38259  atlatmstc  39779  atlatle  39780  glbconN  39837  intnatN  39867  lnnat  39887  atcvrj2b  39892  atexchcvrN  39900  llncvrlpln  40018  lplncvrlvol  40076  lautcvr  40552  trlatn0  40632  cdleme48fvg  40960  cdlemg33c  41168  dihcl  41730  imadomfi  42455  fsuppssind  43040  elpell1qr2  43318  oddcomabszz  43390  wepwsolem  43488  mendring  43634  mendlmod  43635  hausgraph  43651  cantnftermord  43766  cantnfub  43767  cantnf2  43771  omabs2  43778  rp-isfinite5  43962  omelaxinf2  45434  cncmpmax  45481  eliinid  45559  icccncfext  46333  dvnprodlem2  46393  stoweidlem7  46453  stoweidlem34  46480  stoweidlem35  46481  stoweidlem59  46505  stoweidlem60  46506  stoweidlem62  46508  fourierdlem34  46587  fourierdlem73  46625  fourierdlem77  46629  etransclem35  46715  smfsuplem2  47258  pgrple2abl  48853  clddisj  49391