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 484	. 2 ⊢ ((𝜑 ∧ 𝜓) → 𝜓)
3		sylancom.2	. 2 ⊢ ((𝜒 ∧ 𝜓) → 𝜃)
4	1, 2, 3	syl2anc 584	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  6129  ordin  6331  fimacnvdisj  6696  f1oexrnex  7852  wemoiso  7900  wemoiso2  7901  smocdmdom  8283  rdglim  8340  oaabs  8558  ecref  8662  f1oenfi  9083  f1oenfirn  9084  f1domfi  9085  domfi  9093  sdomdomtrfi  9105  php  9111  f1vrnfibi  9221  brwdom2  9454  infdiffi  9543  cantnflem1  9574  wemapwe  9582  cnfcom3lem  9588  r1lim  9660  carduni  9869  ac5num  9922  infunsdom1  10098  cofsmo  10155  isf32lem6  10244  hsmexlem1  10312  ac6c4  10367  fnct  10423  pwfseqlem1  10544  tskuni  10669  recgt1i  12014  avgle2  12357  eluzmn  12734  rpnnen1lem1  12871  xnn0le2is012  13140  fzneuz  13503  mulmod0  13776  hasheni  14250  hashun2  14285  hashf1dmrn  14345  reccn2  15499  isershft  15566  sumeq2ii  15595  prodeq2ii  15813  demoivreALT  16105  bitsp1  16337  gcdneg  16428  eucalginv  16490  eucalg  16493  odzdvds  16702  fldivp1  16804  prmunb  16821  vdwap1  16884  setsid  17113  acsmapd  18455  intopsn  18557  cntzidss  19247  symggrp  19307  pmtrfv  19359  odmodnn0  19447  sylow2alem1  19524  telgsumfzs  19896  dprdsn  19945  dvdsrmul1  20282  dvrid  20319  cntzsubrng  20477  znunit  21495  isphld  21586  frlmup1  21730  evl1val  22239  evl1sca  22244  pf1const  22256  mat1f1o  22388  mat1mhm  22394  matunit  22588  pm2mpmhmlem2  22729  cctop  22916  iscnp4  23173  iscncl  23179  cnntr  23185  tx2cn  23520  xkoco1cn  23567  qtopkgen  23620  hmeontr  23679  hmeores  23681  filssufilg  23821  ustuqtop1  24151  utop2nei  24160  fmucndlem  24200  cfilufg  24202  xmetres2  24271  metres2  24273  metustto  24463  metust  24468  cfilucfil  24469  dscopn  24483  nmoi  24638  iccntr  24732  cphsqrtcl2  25108  cmsss  25273  ivthlem3  25376  sca2rab  25435  ovolicc2lem3  25442  mdegleb  25991  mdegmullem  26005  aalioulem3  26264  ulm2  26316  ulmcn  26330  root1eq1  26687  atanlogsublem  26847  birthdaylem3  26885  logexprlim  27158  dchrisumlem3  27424  f1otrg  28844  ax5seglem1  28901  ax5seglem2  28902  ax5seglem3a  28903  ax5seglem4  28905  ax5seglem9  28910  ax5seg  28911  axbtwnid  28912  axlowdimlem17  28931  axcontlem2  28938  axcontlem4  28940  axcontlem8  28944  cyclnumvtx  29773  rusgrnumwwlks  29947  wwlksext2clwwlk  30029  grpoidinv  30480  imsmetlem  30662  ipasslem1  30803  ip2eqi  30828  hvpncan  31011  pjid  31667  hmopre  31895  eigvalcl  31933  leopnmid  32110  superpos  32326  cvp  32347  rabfodom  32477  xlt2addrd  32734  hashxpe  32781  cyc3genpmlem  33112  lmodslmd  33165  elrgspnlem4  33204  elrgspnsubrunlem2  33207  nsgqusf1olem2  33371  elrspunidl  33385  prmidl0  33407  rsprprmprmidlb  33480  extdgfialglem1  33697  irngnminplynz  33717  constrfiss  33756  locfinreflem  33845  zarcls0  33873  fmcncfil  33936  rge0scvg  33954  esumfsup  34075  esumcvg  34091  insiga  34142  ballotlemirc  34537  signstfvcl  34578  signsvfn  34587  upgracycusgr  35191  subfacp1lem6  35221  satfdmlem  35404  msubff1  35592  fv2ndcnv  35814  matunitlindf  37658  ovoliunnfl  37702  voliunnfl  37704  volsupnfl  37705  ftc1anclem5  37737  indexa  37773  sstotbnd3  37816  heiborlem6  37856  rngosn3  37964  atlatmstc  39358  atlatle  39359  glbconN  39416  intnatN  39446  lnnat  39466  atcvrj2b  39471  atexchcvrN  39479  llncvrlpln  39597  lplncvrlvol  39655  lautcvr  40131  trlatn0  40211  cdleme48fvg  40539  cdlemg33c  40747  dihcl  41309  imadomfi  42035  fsuppssind  42626  elpell1qr2  42905  oddcomabszz  42977  wepwsolem  43075  mendring  43221  mendlmod  43222  hausgraph  43238  cantnftermord  43353  cantnfub  43354  cantnf2  43358  omabs2  43365  rp-isfinite5  43550  omelaxinf2  45022  cncmpmax  45069  eliinid  45148  icccncfext  45925  dvnprodlem2  45985  stoweidlem7  46045  stoweidlem34  46072  stoweidlem35  46073  stoweidlem59  46097  stoweidlem60  46098  stoweidlem62  46100  fourierdlem34  46179  fourierdlem73  46217  fourierdlem77  46221  etransclem35  46307  smfsuplem2  46850  pgrple2abl  48396  clddisj  48935