Theorem sylancom 578

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

Syntax hints:   → wi 4   ∧ wa 384

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 198  df-an 385

This theorem is referenced by:  adant423OLD  863  sofld  5786  ordin  5960  fimacnvdisj  6292  f1oexrnex  7339  wemoiso  7377  wemoiso2  7378  smorndom  7695  rdglim  7752  oaabs  7955  ssct  8274  onomeneq  8383  domfi  8414  f1vrnfibi  8484  brwdom2  8711  infdiffi  8796  cantnflem1  8827  wemapwe  8835  cnfcom3lem  8841  r1lim  8876  carduni  9084  ac5num  9136  infunsdom1  9314  cofsmo  9370  isf32lem6  9459  hsmexlem1  9527  ac6c4  9582  fnct  9638  pwfseqlem1  9759  tskuni  9884  recgt1i  11199  avgle2  11534  eluzmn  11905  rpnnen1lem1  12028  xnn0le2is012  12288  ioodisj  12519  fzneuz  12638  mulmod0  12894  hasheni  13350  hashun2  13384  swrdccatin1  13701  reccn2  14544  isershft  14611  sumeq2ii  14640  prodeq2ii  14858  demoivreALT  15145  bitsp1  15366  gcdneg  15456  eucalginv  15510  eucalg  15513  odzdvds  15711  fldivp1  15812  prmunb  15829  vdwap1  15892  setsid  16119  funcsetcestrclem7  17000  acsmapd  17377  intopsn  17452  cntzidss  17965  symggrp  18015  odmodnn0  18154  sylow2alem1  18227  telgsumfzs  18582  dprdsn  18631  dvdsrmul1  18849  dvrid  18884  evl1val  19895  evl1sca  19900  pf1const  19912  znunit  20113  isphld  20203  frlmup1  20341  mat1f1o  20489  mat1mhm  20495  matunit  20690  pm2mpmhmlem2  20831  cctop  21018  iscnp4  21275  iscncl  21281  cnntr  21287  tx2cn  21621  xkoco1cn  21668  qtopkgen  21721  hmeontr  21780  hmeores  21782  filssufilg  21922  ustuqtop1  22252  ustuqtop2  22253  utop2nei  22261  fmucndlem  22302  cfilufg  22304  xmetres2  22373  metres2  22375  metustto  22565  cfilucfil  22571  dscopn  22585  nmoi  22739  iccntr  22831  cphsqrtcl2  23192  cmsss  23353  ivthlem3  23428  sca2rab  23487  ovolicc2lem3  23494  mdegleb  24032  aalioulem3  24297  ulm2  24347  ulmcn  24361  root1eq1  24704  atanlogsublem  24850  birthdaylem3  24888  logexprlim  25158  dchrisumlem3  25388  tglowdim1i  25604  f1otrg  25959  f1otrge  25960  ax5seglem1  26016  ax5seglem2  26017  ax5seglem3a  26018  ax5seglem4  26020  ax5seglem9  26025  ax5seg  26026  axbtwnid  26027  axlowdimlem17  26046  axcontlem2  26053  axcontlem4  26055  axcontlem8  26059  rusgrnumwwlks  27110  grpoidinv  27685  imsmetlem  27867  ipasslem1  28008  ip2eqi  28034  hvpncan  28218  pjid  28876  hmopre  29104  eigvalcl  29142  leopnmid  29319  superpos  29535  cvp  29556  rabfodom  29663  xlt2addrd  29844  lmodslmd  30076  locfinreflem  30226  prsdm  30279  prsrn  30280  fmcncfil  30296  rge0scvg  30314  esumfsup  30451  esumcvg  30467  insiga  30519  ballotlemirc  30912  signstfvcl  30969  subfacp1lem6  31484  msubff1  31770  fv2ndcnv  31995  matunitlindf  33714  ovoliunnfl  33758  voliunnfl  33760  volsupnfl  33761  ftc1anclem5  33795  indexa  33834  sstotbnd3  33880  heiborlem6  33920  rngosn3  34028  atlatmstc  35093  atlatle  35094  glbconN  35151  intnatN  35181  lnnat  35201  atcvrj2b  35206  atexchcvrN  35214  llncvrlpln  35332  lplncvrlvol  35390  lautcvr  35866  trlatn0  35947  cdleme48fvg  36275  cdlemg33c  36483  dihcl  37045  elpell1qr2  37932  oddcomabszz  38004  wepwsolem  38107  mendring  38257  mendlmod  38258  hausgraph  38285  rp-isfinite5  38357  cncmpmax  39679  eliinid  39780  icccncfext  40574  dvnprodlem2  40636  stoweidlem7  40697  stoweidlem34  40724  stoweidlem35  40725  stoweidlem59  40749  stoweidlem60  40750  stoweidlem62  40752  fourierdlem34  40831  fourierdlem73  40869  fourierdlem77  40873  etransclem35  40959  smfsuplem2  41494  pgrple2abl  42708