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  6151  ordin  6353  fimacnvdisj  6718  f1oexrnex  7878  wemoiso  7926  wemoiso2  7927  smocdmdom  8308  rdglim  8365  oaabs  8584  ecref  8689  f1oenfi  9113  f1oenfirn  9114  f1domfi  9115  domfi  9123  sdomdomtrfi  9135  php  9141  f1vrnfibi  9252  brwdom2  9488  infdiffi  9579  cantnflem1  9610  wemapwe  9618  cnfcom3lem  9624  r1lim  9696  carduni  9905  ac5num  9958  infunsdom1  10134  cofsmo  10191  isf32lem6  10280  hsmexlem1  10348  ac6c4  10403  fnct  10459  pwfseqlem1  10581  tskuni  10706  recgt1i  12053  avgle2  12418  eluzmn  12795  rpnnen1lem1  12928  xnn0le2is012  13198  fzneuz  13562  mulmod0  13836  hasheni  14310  hashun2  14345  hashf1dmrn  14405  reccn2  15559  isershft  15626  sumeq2ii  15655  prodeq2ii  15876  demoivreALT  16168  bitsp1  16400  gcdneg  16491  eucalginv  16553  eucalg  16556  odzdvds  16766  fldivp1  16868  prmunb  16885  vdwap1  16948  setsid  17177  acsmapd  18520  intopsn  18622  cntzidss  19315  symggrp  19375  pmtrfv  19427  odmodnn0  19515  sylow2alem1  19592  telgsumfzs  19964  dprdsn  20013  dvdsrmul1  20349  dvrid  20386  cntzsubrng  20544  znunit  21543  isphld  21634  frlmup1  21778  evl1val  22294  evl1sca  22299  pf1const  22311  mat1f1o  22443  mat1mhm  22449  matunit  22643  pm2mpmhmlem2  22784  cctop  22971  iscnp4  23228  iscncl  23234  cnntr  23240  tx2cn  23575  xkoco1cn  23622  qtopkgen  23675  hmeontr  23734  hmeores  23736  filssufilg  23876  ustuqtop1  24206  utop2nei  24215  fmucndlem  24255  cfilufg  24257  xmetres2  24326  metres2  24328  metustto  24518  metust  24523  cfilucfil  24524  dscopn  24538  nmoi  24693  iccntr  24787  cphsqrtcl2  25153  cmsss  25318  ivthlem3  25420  sca2rab  25479  ovolicc2lem3  25486  mdegleb  26029  mdegmullem  26043  aalioulem3  26300  ulm2  26350  ulmcn  26364  root1eq1  26719  atanlogsublem  26879  birthdaylem3  26917  logexprlim  27188  dchrisumlem3  27454  f1otrg  28939  ax5seglem1  28997  ax5seglem2  28998  ax5seglem3a  28999  ax5seglem4  29001  ax5seglem9  29006  ax5seg  29007  axbtwnid  29008  axlowdimlem17  29027  axcontlem2  29034  axcontlem4  29036  axcontlem8  29040  cyclnumvtx  29868  rusgrnumwwlks  30045  wwlksext2clwwlk  30127  grpoidinv  30579  imsmetlem  30761  ipasslem1  30902  ip2eqi  30927  hvpncan  31110  pjid  31766  hmopre  31994  eigvalcl  32032  leopnmid  32209  superpos  32425  cvp  32446  rabfodom  32575  xlt2addrd  32832  hashxpe  32880  suppgsumssiun  33133  cyc3genpmlem  33212  lmodslmd  33265  elrgspnlem4  33306  elrgspnsubrunlem2  33309  nsgqusf1olem2  33474  elrspunidl  33488  prmidl0  33510  rsprprmprmidlb  33583  extdgfialglem1  33836  irngnminplynz  33856  constrfiss  33895  locfinreflem  33984  zarcls0  34012  fmcncfil  34075  rge0scvg  34093  esumfsup  34214  esumcvg  34230  insiga  34281  ballotlemirc  34676  signstfvcl  34717  signsvfn  34726  upgracycusgr  35337  subfacp1lem6  35367  satfdmlem  35550  msubff1  35738  fv2ndcnv  35960  matunitlindf  37939  ovoliunnfl  37983  voliunnfl  37985  volsupnfl  37986  ftc1anclem5  38018  indexa  38054  sstotbnd3  38097  heiborlem6  38137  rngosn3  38245  atlatmstc  39765  atlatle  39766  glbconN  39823  intnatN  39853  lnnat  39873  atcvrj2b  39878  atexchcvrN  39886  llncvrlpln  40004  lplncvrlvol  40062  lautcvr  40538  trlatn0  40618  cdleme48fvg  40946  cdlemg33c  41154  dihcl  41716  imadomfi  42441  fsuppssind  43026  elpell1qr2  43300  oddcomabszz  43372  wepwsolem  43470  mendring  43616  mendlmod  43617  hausgraph  43633  cantnftermord  43748  cantnfub  43749  cantnf2  43753  omabs2  43760  rp-isfinite5  43944  omelaxinf2  45416  cncmpmax  45463  eliinid  45541  icccncfext  46315  dvnprodlem2  46375  stoweidlem7  46435  stoweidlem34  46462  stoweidlem35  46463  stoweidlem59  46487  stoweidlem60  46488  stoweidlem62  46490  fourierdlem34  46569  fourierdlem73  46607  fourierdlem77  46611  etransclem35  46697  smfsuplem2  47240  pgrple2abl  48841  clddisj  49379