Theorem sylancom 590

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

Syntax hints:   → wi 4   ∧ wa 398

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 209  df-an 399

This theorem is referenced by:  sofld  6039  ordin  6216  fimacnvdisj  6552  f1oexrnex  7626  wemoiso  7668  wemoiso2  7669  smorndom  7999  rdglim  8056  oaabs  8265  ssct  8592  onomeneq  8702  domfi  8733  f1vrnfibi  8803  brwdom2  9031  infdiffi  9115  cantnflem1  9146  wemapwe  9154  cnfcom3lem  9160  r1lim  9195  carduni  9404  ac5num  9456  infunsdom1  9629  cofsmo  9685  isf32lem6  9774  hsmexlem1  9842  ac6c4  9897  fnct  9953  pwfseqlem1  10074  tskuni  10199  recgt1i  11531  avgle2  11872  eluzmn  12244  rpnnen1lem1  12371  xnn0le2is012  12633  fzneuz  12982  mulmod0  13239  hasheni  13702  hashun2  13738  reccn2  14947  isershft  15014  sumeq2ii  15044  prodeq2ii  15261  demoivreALT  15548  bitsp1  15774  gcdneg  15864  eucalginv  15922  eucalg  15925  odzdvds  16126  fldivp1  16227  prmunb  16244  vdwap1  16307  setsid  16532  acsmapd  17782  intopsn  17858  cntzidss  18462  symggrp  18522  pmtrfv  18574  odmodnn0  18662  sylow2alem1  18736  telgsumfzs  19103  dprdsn  19152  dvdsrmul1  19397  dvrid  19432  evl1val  20486  evl1sca  20491  pf1const  20503  znunit  20704  isphld  20792  frlmup1  20936  mat1f1o  21081  mat1mhm  21087  matunit  21281  pm2mpmhmlem2  21421  cctop  21608  iscnp4  21865  iscncl  21871  cnntr  21877  tx2cn  22212  xkoco1cn  22259  qtopkgen  22312  hmeontr  22371  hmeores  22373  filssufilg  22513  ustuqtop1  22844  utop2nei  22853  fmucndlem  22894  cfilufg  22896  xmetres2  22965  metres2  22967  metustto  23157  metust  23162  cfilucfil  23163  dscopn  23177  nmoi  23331  iccntr  23423  cphsqrtcl2  23784  cmsss  23948  ivthlem3  24048  sca2rab  24107  ovolicc2lem3  24114  mdegleb  24652  aalioulem3  24917  ulm2  24967  ulmcn  24981  root1eq1  25330  atanlogsublem  25487  birthdaylem3  25525  logexprlim  25795  dchrisumlem3  26061  f1otrg  26651  ax5seglem1  26708  ax5seglem2  26709  ax5seglem3a  26710  ax5seglem4  26712  ax5seglem9  26717  ax5seg  26718  axbtwnid  26719  axlowdimlem17  26738  axcontlem2  26745  axcontlem4  26747  axcontlem8  26751  rusgrnumwwlks  27747  wwlksext2clwwlk  27830  grpoidinv  28279  imsmetlem  28461  ipasslem1  28602  ip2eqi  28627  hvpncan  28810  pjid  29466  hmopre  29694  eigvalcl  29732  leopnmid  29909  superpos  30125  cvp  30146  rabfodom  30260  xlt2addrd  30476  hashxpe  30523  cyc3genpmlem  30788  lmodslmd  30827  locfinreflem  31099  fmcncfil  31169  rge0scvg  31187  esumfsup  31324  esumcvg  31340  insiga  31391  ballotlemirc  31784  signstfvcl  31838  signsvfn  31847  hashf1dmrn  32350  upgracycusgr  32397  subfacp1lem6  32427  satfdmlem  32610  msubff1  32798  fv2ndcnv  33016  matunitlindf  34884  ovoliunnfl  34928  voliunnfl  34930  volsupnfl  34931  ftc1anclem5  34965  indexa  35002  sstotbnd3  35048  heiborlem6  35088  rngosn3  35196  atlatmstc  36449  atlatle  36450  glbconN  36507  intnatN  36537  lnnat  36557  atcvrj2b  36562  atexchcvrN  36570  llncvrlpln  36688  lplncvrlvol  36746  lautcvr  37222  trlatn0  37302  cdleme48fvg  37630  cdlemg33c  37838  dihcl  38400  elpell1qr2  39462  oddcomabszz  39534  wepwsolem  39635  mendring  39785  mendlmod  39786  hausgraph  39805  rp-isfinite5  39876  cncmpmax  41282  eliinid  41370  icccncfext  42162  dvnprodlem2  42224  stoweidlem7  42285  stoweidlem34  42312  stoweidlem35  42313  stoweidlem59  42337  stoweidlem60  42338  stoweidlem62  42340  fourierdlem34  42419  fourierdlem73  42457  fourierdlem77  42461  etransclem35  42547  smfsuplem2  43079  pgrple2abl  44406