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  6176  ordin  6382  fimacnvdisj  6756  f1oexrnex  7923  wemoiso  7972  wemoiso2  7973  smocdmdom  8382  rdglim  8440  oaabs  8660  ecref  8764  ssctOLD  9066  f1oenfi  9193  f1oenfirn  9194  f1domfi  9195  domfi  9203  sdomdomtrfi  9215  php  9221  onomeneqOLD  9238  f1vrnfibi  9354  brwdom2  9587  infdiffi  9672  cantnflem1  9703  wemapwe  9711  cnfcom3lem  9717  r1lim  9786  carduni  9995  ac5num  10050  infunsdom1  10226  cofsmo  10283  isf32lem6  10372  hsmexlem1  10440  ac6c4  10495  fnct  10551  pwfseqlem1  10672  tskuni  10797  recgt1i  12139  avgle2  12482  eluzmn  12859  rpnnen1lem1  12994  xnn0le2is012  13262  fzneuz  13625  mulmod0  13894  hasheni  14366  hashun2  14401  hashf1dmrn  14461  reccn2  15613  isershft  15680  sumeq2ii  15709  prodeq2ii  15927  demoivreALT  16219  bitsp1  16450  gcdneg  16541  eucalginv  16603  eucalg  16606  odzdvds  16815  fldivp1  16917  prmunb  16934  vdwap1  16997  setsid  17226  acsmapd  18564  intopsn  18632  cntzidss  19323  symggrp  19381  pmtrfv  19433  odmodnn0  19521  sylow2alem1  19598  telgsumfzs  19970  dprdsn  20019  dvdsrmul1  20329  dvrid  20366  cntzsubrng  20527  znunit  21524  isphld  21614  frlmup1  21758  evl1val  22267  evl1sca  22272  pf1const  22284  mat1f1o  22416  mat1mhm  22422  matunit  22616  pm2mpmhmlem2  22757  cctop  22944  iscnp4  23201  iscncl  23207  cnntr  23213  tx2cn  23548  xkoco1cn  23595  qtopkgen  23648  hmeontr  23707  hmeores  23709  filssufilg  23849  ustuqtop1  24180  utop2nei  24189  fmucndlem  24229  cfilufg  24231  xmetres2  24300  metres2  24302  metustto  24492  metust  24497  cfilucfil  24498  dscopn  24512  nmoi  24667  iccntr  24761  cphsqrtcl2  25138  cmsss  25303  ivthlem3  25406  sca2rab  25465  ovolicc2lem3  25472  mdegleb  26021  mdegmullem  26035  aalioulem3  26294  ulm2  26346  ulmcn  26360  root1eq1  26717  atanlogsublem  26877  birthdaylem3  26915  logexprlim  27188  dchrisumlem3  27454  f1otrg  28850  ax5seglem1  28907  ax5seglem2  28908  ax5seglem3a  28909  ax5seglem4  28911  ax5seglem9  28916  ax5seg  28917  axbtwnid  28918  axlowdimlem17  28937  axcontlem2  28944  axcontlem4  28946  axcontlem8  28950  cyclnumvtx  29782  rusgrnumwwlks  29956  wwlksext2clwwlk  30038  grpoidinv  30489  imsmetlem  30671  ipasslem1  30812  ip2eqi  30837  hvpncan  31020  pjid  31676  hmopre  31904  eigvalcl  31942  leopnmid  32119  superpos  32335  cvp  32356  rabfodom  32486  xlt2addrd  32736  hashxpe  32786  cyc3genpmlem  33162  lmodslmd  33201  elrgspnlem4  33240  elrgspnsubrunlem2  33243  nsgqusf1olem2  33429  elrspunidl  33443  prmidl0  33465  rsprprmprmidlb  33538  irngnminplynz  33746  constrfiss  33785  locfinreflem  33871  zarcls0  33899  fmcncfil  33962  rge0scvg  33980  esumfsup  34101  esumcvg  34117  insiga  34168  ballotlemirc  34564  signstfvcl  34605  signsvfn  34614  upgracycusgr  35177  subfacp1lem6  35207  satfdmlem  35390  msubff1  35578  fv2ndcnv  35795  matunitlindf  37642  ovoliunnfl  37686  voliunnfl  37688  volsupnfl  37689  ftc1anclem5  37721  indexa  37757  sstotbnd3  37800  heiborlem6  37840  rngosn3  37948  atlatmstc  39337  atlatle  39338  glbconN  39395  glbconNOLD  39396  intnatN  39426  lnnat  39446  atcvrj2b  39451  atexchcvrN  39459  llncvrlpln  39577  lplncvrlvol  39635  lautcvr  40111  trlatn0  40191  cdleme48fvg  40519  cdlemg33c  40727  dihcl  41289  imadomfi  42015  fsuppssind  42616  elpell1qr2  42895  oddcomabszz  42968  wepwsolem  43066  mendring  43212  mendlmod  43213  hausgraph  43229  cantnftermord  43344  cantnfub  43345  cantnf2  43349  omabs2  43356  rp-isfinite5  43541  omelaxinf2  45014  cncmpmax  45056  eliinid  45135  icccncfext  45916  dvnprodlem2  45976  stoweidlem7  46036  stoweidlem34  46063  stoweidlem35  46064  stoweidlem59  46088  stoweidlem60  46089  stoweidlem62  46091  fourierdlem34  46170  fourierdlem73  46208  fourierdlem77  46212  etransclem35  46298  smfsuplem2  46841  pgrple2abl  48340  clddisj  48878