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  6207  ordin  6414  fimacnvdisj  6786  f1oexrnex  7949  wemoiso  7998  wemoiso2  7999  smocdmdom  8408  rdglim  8466  oaabs  8686  ecref  8790  ssctOLD  9092  f1oenfi  9219  f1oenfirn  9220  f1domfi  9221  domfi  9229  sdomdomtrfi  9241  php  9247  onomeneqOLD  9266  f1vrnfibi  9382  brwdom2  9613  infdiffi  9698  cantnflem1  9729  wemapwe  9737  cnfcom3lem  9743  r1lim  9812  carduni  10021  ac5num  10076  infunsdom1  10252  cofsmo  10309  isf32lem6  10398  hsmexlem1  10466  ac6c4  10521  fnct  10577  pwfseqlem1  10698  tskuni  10823  recgt1i  12165  avgle2  12507  eluzmn  12885  rpnnen1lem1  13020  xnn0le2is012  13288  fzneuz  13648  mulmod0  13917  hasheni  14387  hashun2  14422  hashf1dmrn  14482  reccn2  15633  isershft  15700  sumeq2ii  15729  prodeq2ii  15947  demoivreALT  16237  bitsp1  16468  gcdneg  16559  eucalginv  16621  eucalg  16624  odzdvds  16833  fldivp1  16935  prmunb  16952  vdwap1  17015  setsid  17244  acsmapd  18599  intopsn  18667  cntzidss  19358  symggrp  19418  pmtrfv  19470  odmodnn0  19558  sylow2alem1  19635  telgsumfzs  20007  dprdsn  20056  dvdsrmul1  20369  dvrid  20406  cntzsubrng  20567  znunit  21582  isphld  21672  frlmup1  21818  evl1val  22333  evl1sca  22338  pf1const  22350  mat1f1o  22484  mat1mhm  22490  matunit  22684  pm2mpmhmlem2  22825  cctop  23013  iscnp4  23271  iscncl  23277  cnntr  23283  tx2cn  23618  xkoco1cn  23665  qtopkgen  23718  hmeontr  23777  hmeores  23779  filssufilg  23919  ustuqtop1  24250  utop2nei  24259  fmucndlem  24300  cfilufg  24302  xmetres2  24371  metres2  24373  metustto  24566  metust  24571  cfilucfil  24572  dscopn  24586  nmoi  24749  iccntr  24843  cphsqrtcl2  25220  cmsss  25385  ivthlem3  25488  sca2rab  25547  ovolicc2lem3  25554  mdegleb  26103  mdegmullem  26117  aalioulem3  26376  ulm2  26428  ulmcn  26442  root1eq1  26798  atanlogsublem  26958  birthdaylem3  26996  logexprlim  27269  dchrisumlem3  27535  f1otrg  28879  ax5seglem1  28943  ax5seglem2  28944  ax5seglem3a  28945  ax5seglem4  28947  ax5seglem9  28952  ax5seg  28953  axbtwnid  28954  axlowdimlem17  28973  axcontlem2  28980  axcontlem4  28982  axcontlem8  28986  cyclnumvtx  29820  rusgrnumwwlks  29994  wwlksext2clwwlk  30076  grpoidinv  30527  imsmetlem  30709  ipasslem1  30850  ip2eqi  30875  hvpncan  31058  pjid  31714  hmopre  31942  eigvalcl  31980  leopnmid  32157  superpos  32373  cvp  32394  rabfodom  32524  xlt2addrd  32762  hashxpe  32811  cyc3genpmlem  33171  lmodslmd  33210  elrgspnlem4  33249  elrgspnsubrunlem2  33252  nsgqusf1olem2  33442  elrspunidl  33456  prmidl0  33478  rsprprmprmidlb  33551  irngnminplynz  33755  locfinreflem  33839  zarcls0  33867  fmcncfil  33930  rge0scvg  33948  esumfsup  34071  esumcvg  34087  insiga  34138  ballotlemirc  34534  signstfvcl  34588  signsvfn  34597  upgracycusgr  35160  subfacp1lem6  35190  satfdmlem  35373  msubff1  35561  fv2ndcnv  35778  matunitlindf  37625  ovoliunnfl  37669  voliunnfl  37671  volsupnfl  37672  ftc1anclem5  37704  indexa  37740  sstotbnd3  37783  heiborlem6  37823  rngosn3  37931  atlatmstc  39320  atlatle  39321  glbconN  39378  glbconNOLD  39379  intnatN  39409  lnnat  39429  atcvrj2b  39434  atexchcvrN  39442  llncvrlpln  39560  lplncvrlvol  39618  lautcvr  40094  trlatn0  40174  cdleme48fvg  40502  cdlemg33c  40710  dihcl  41272  imadomfi  42003  fsuppssind  42603  elpell1qr2  42883  oddcomabszz  42956  wepwsolem  43054  mendring  43200  mendlmod  43201  hausgraph  43217  cantnftermord  43333  cantnfub  43334  cantnf2  43338  omabs2  43345  rp-isfinite5  43530  omelaxinf2  45006  cncmpmax  45037  eliinid  45116  icccncfext  45902  dvnprodlem2  45962  stoweidlem7  46022  stoweidlem34  46049  stoweidlem35  46050  stoweidlem59  46074  stoweidlem60  46075  stoweidlem62  46077  fourierdlem34  46156  fourierdlem73  46194  fourierdlem77  46198  etransclem35  46284  smfsuplem2  46827  pgrple2abl  48281  clddisj  48801