Theorem sylancom 701

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 477	. 2 ⊢ ((𝜑 ∧ 𝜓) → 𝜓)
3		sylancom.2	. 2 ⊢ ((𝜒 ∧ 𝜓) → 𝜃)
4	1, 2, 3	syl2anc 693	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 197  df-an 386

This theorem is referenced by:  adant423OLD  823  sofld  5581  ordin  5753  fimacnvdisj  6083  f1oexrnex  7115  wemoiso  7153  wemoiso2  7154  smorndom  7465  rdglim  7522  oaabs  7724  ssct  8041  onomeneq  8150  domfi  8181  f1vrnfibi  8251  brwdom2  8478  infdiffi  8555  cantnflem1  8586  wemapwe  8594  cnfcom3lem  8600  r1lim  8635  carduni  8807  ac5num  8859  infunsdom1  9035  cofsmo  9091  isf32lem6  9180  hsmexlem1  9248  ac6c4  9303  fnct  9359  pwfseqlem1  9480  tskuni  9605  recgt1i  10920  avgle2  11273  eluzmn  11694  rpnnen1lem1  11815  rpnnen1lem1OLD  11821  xnn0le2is012  12076  ioodisj  12302  fzneuz  12421  mulmod0  12676  hasheni  13136  hashun2  13172  swrdccatin1  13483  reccn2  14327  isershft  14394  sumeq2ii  14423  prodeq2ii  14643  demoivreALT  14931  bitsp1  15153  gcdneg  15243  eucalginv  15297  eucalg  15300  odzdvds  15500  fldivp1  15601  prmunb  15618  vdwap1  15681  setsid  15914  funcsetcestrclem7  16801  acsmapd  17178  intopsn  17253  cntzidss  17770  symggrp  17820  odmodnn0  17959  sylow2alem1  18032  telgsumfzs  18386  dprdsn  18435  dvdsrmul1  18653  dvrid  18688  evl1val  19693  evl1sca  19698  pf1const  19710  znunit  19912  isphld  19999  frlmup1  20137  mat1f1o  20284  mat1mhm  20290  matunit  20484  pm2mpmhmlem2  20624  cctop  20810  iscnp4  21067  iscncl  21073  cnntr  21079  tx2cn  21413  xkoco1cn  21460  qtopkgen  21513  hmeontr  21572  hmeores  21574  filssufilg  21715  ustuqtop1  22045  ustuqtop2  22046  utop2nei  22054  fmucndlem  22095  cfilufg  22097  xmetres2  22166  metres2  22168  metustto  22358  cfilucfil  22364  dscopn  22378  nmoi  22532  iccntr  22624  cphsqrtcl2  22986  cmsss  23147  ivthlem3  23222  sca2rab  23280  ovolicc2lem3  23287  mdegleb  23824  aalioulem3  24089  ulm2  24139  ulmcn  24153  root1eq1  24496  atanlogsublem  24642  birthdaylem3  24680  logexprlim  24950  dchrisumlem3  25180  tglowdim1i  25396  f1otrg  25751  f1otrge  25752  ax5seglem1  25808  ax5seglem2  25809  ax5seglem3a  25810  ax5seglem4  25812  ax5seglem9  25817  ax5seg  25818  axbtwnid  25819  axlowdimlem17  25838  axcontlem2  25845  axcontlem4  25847  axcontlem8  25851  rusgrnumwwlks  26869  grpoidinv  27362  imsmetlem  27545  ipasslem1  27686  ip2eqi  27712  hvpncan  27896  pjid  28554  hmopre  28782  eigvalcl  28820  leopnmid  28997  superpos  29213  cvp  29234  rabfodom  29344  xlt2addrd  29523  lmodslmd  29757  locfinreflem  29907  prsdm  29960  prsrn  29961  fmcncfil  29977  rge0scvg  29995  esumfsup  30132  esumcvg  30148  insiga  30200  ballotlemirc  30593  signstfvcl  30650  subfacp1lem6  31167  msubff1  31453  fv2ndcnv  31681  matunitlindf  33407  ovoliunnfl  33451  voliunnfl  33453  volsupnfl  33454  ftc1anclem5  33489  indexa  33528  sstotbnd3  33575  heiborlem6  33615  rngosn3  33723  atlatmstc  34606  atlatle  34607  glbconN  34663  intnatN  34693  lnnat  34713  atcvrj2b  34718  atexchcvrN  34726  llncvrlpln  34844  lplncvrlvol  34902  lautcvr  35378  trlatn0  35459  cdleme48fvg  35788  cdlemg33c  35996  dihcl  36559  elpell1qr2  37436  oddcomabszz  37509  wepwsolem  37612  mendring  37762  mendlmod  37763  hausgraph  37790  rp-isfinite5  37863  cncmpmax  39191  eliinid  39294  icccncfext  40100  dvnprodlem2  40162  stoweidlem7  40224  stoweidlem34  40251  stoweidlem35  40252  stoweidlem59  40276  stoweidlem60  40277  stoweidlem62  40279  fourierdlem34  40358  fourierdlem73  40396  fourierdlem77  40400  etransclem35  40486  smfsuplem2  41018  pgrple2abl  42146