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  6163  ordin  6365  fimacnvdisj  6741  f1oexrnex  7906  wemoiso  7955  wemoiso2  7956  smocdmdom  8340  rdglim  8397  oaabs  8615  ecref  8719  ssctOLD  9026  f1oenfi  9149  f1oenfirn  9150  f1domfi  9151  domfi  9159  sdomdomtrfi  9171  php  9177  f1vrnfibi  9300  brwdom2  9533  infdiffi  9618  cantnflem1  9649  wemapwe  9657  cnfcom3lem  9663  r1lim  9732  carduni  9941  ac5num  9996  infunsdom1  10172  cofsmo  10229  isf32lem6  10318  hsmexlem1  10386  ac6c4  10441  fnct  10497  pwfseqlem1  10618  tskuni  10743  recgt1i  12087  avgle2  12430  eluzmn  12807  rpnnen1lem1  12944  xnn0le2is012  13213  fzneuz  13576  mulmod0  13846  hasheni  14320  hashun2  14355  hashf1dmrn  14415  reccn2  15570  isershft  15637  sumeq2ii  15666  prodeq2ii  15884  demoivreALT  16176  bitsp1  16408  gcdneg  16499  eucalginv  16561  eucalg  16564  odzdvds  16773  fldivp1  16875  prmunb  16892  vdwap1  16955  setsid  17184  acsmapd  18520  intopsn  18588  cntzidss  19279  symggrp  19337  pmtrfv  19389  odmodnn0  19477  sylow2alem1  19554  telgsumfzs  19926  dprdsn  19975  dvdsrmul1  20285  dvrid  20322  cntzsubrng  20483  znunit  21480  isphld  21570  frlmup1  21714  evl1val  22223  evl1sca  22228  pf1const  22240  mat1f1o  22372  mat1mhm  22378  matunit  22572  pm2mpmhmlem2  22713  cctop  22900  iscnp4  23157  iscncl  23163  cnntr  23169  tx2cn  23504  xkoco1cn  23551  qtopkgen  23604  hmeontr  23663  hmeores  23665  filssufilg  23805  ustuqtop1  24136  utop2nei  24145  fmucndlem  24185  cfilufg  24187  xmetres2  24256  metres2  24258  metustto  24448  metust  24453  cfilucfil  24454  dscopn  24468  nmoi  24623  iccntr  24717  cphsqrtcl2  25093  cmsss  25258  ivthlem3  25361  sca2rab  25420  ovolicc2lem3  25427  mdegleb  25976  mdegmullem  25990  aalioulem3  26249  ulm2  26301  ulmcn  26315  root1eq1  26672  atanlogsublem  26832  birthdaylem3  26870  logexprlim  27143  dchrisumlem3  27409  f1otrg  28805  ax5seglem1  28862  ax5seglem2  28863  ax5seglem3a  28864  ax5seglem4  28866  ax5seglem9  28871  ax5seg  28872  axbtwnid  28873  axlowdimlem17  28892  axcontlem2  28899  axcontlem4  28901  axcontlem8  28905  cyclnumvtx  29737  rusgrnumwwlks  29911  wwlksext2clwwlk  29993  grpoidinv  30444  imsmetlem  30626  ipasslem1  30767  ip2eqi  30792  hvpncan  30975  pjid  31631  hmopre  31859  eigvalcl  31897  leopnmid  32074  superpos  32290  cvp  32311  rabfodom  32441  xlt2addrd  32689  hashxpe  32739  cyc3genpmlem  33115  lmodslmd  33164  elrgspnlem4  33203  elrgspnsubrunlem2  33206  nsgqusf1olem2  33392  elrspunidl  33406  prmidl0  33428  rsprprmprmidlb  33501  irngnminplynz  33709  constrfiss  33748  locfinreflem  33837  zarcls0  33865  fmcncfil  33928  rge0scvg  33946  esumfsup  34067  esumcvg  34083  insiga  34134  ballotlemirc  34530  signstfvcl  34571  signsvfn  34580  upgracycusgr  35149  subfacp1lem6  35179  satfdmlem  35362  msubff1  35550  fv2ndcnv  35772  matunitlindf  37619  ovoliunnfl  37663  voliunnfl  37665  volsupnfl  37666  ftc1anclem5  37698  indexa  37734  sstotbnd3  37777  heiborlem6  37817  rngosn3  37925  atlatmstc  39319  atlatle  39320  glbconN  39377  glbconNOLD  39378  intnatN  39408  lnnat  39428  atcvrj2b  39433  atexchcvrN  39441  llncvrlpln  39559  lplncvrlvol  39617  lautcvr  40093  trlatn0  40173  cdleme48fvg  40501  cdlemg33c  40709  dihcl  41271  imadomfi  41997  fsuppssind  42588  elpell1qr2  42867  oddcomabszz  42940  wepwsolem  43038  mendring  43184  mendlmod  43185  hausgraph  43201  cantnftermord  43316  cantnfub  43317  cantnf2  43321  omabs2  43328  rp-isfinite5  43513  omelaxinf2  44986  cncmpmax  45033  eliinid  45112  icccncfext  45892  dvnprodlem2  45952  stoweidlem7  46012  stoweidlem34  46039  stoweidlem35  46040  stoweidlem59  46064  stoweidlem60  46065  stoweidlem62  46067  fourierdlem34  46146  fourierdlem73  46184  fourierdlem77  46188  etransclem35  46274  smfsuplem2  46817  pgrple2abl  48357  clddisj  48896