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  6145  ordin  6347  fimacnvdisj  6712  f1oexrnex  7869  wemoiso  7917  wemoiso2  7918  smocdmdom  8300  rdglim  8357  oaabs  8576  ecref  8680  f1oenfi  9103  f1oenfirn  9104  f1domfi  9105  domfi  9113  sdomdomtrfi  9125  php  9131  f1vrnfibi  9242  brwdom2  9478  infdiffi  9567  cantnflem1  9598  wemapwe  9606  cnfcom3lem  9612  r1lim  9684  carduni  9893  ac5num  9946  infunsdom1  10122  cofsmo  10179  isf32lem6  10268  hsmexlem1  10336  ac6c4  10391  fnct  10447  pwfseqlem1  10569  tskuni  10694  recgt1i  12039  avgle2  12382  eluzmn  12758  rpnnen1lem1  12891  xnn0le2is012  13161  fzneuz  13524  mulmod0  13797  hasheni  14271  hashun2  14306  hashf1dmrn  14366  reccn2  15520  isershft  15587  sumeq2ii  15616  prodeq2ii  15834  demoivreALT  16126  bitsp1  16358  gcdneg  16449  eucalginv  16511  eucalg  16514  odzdvds  16723  fldivp1  16825  prmunb  16842  vdwap1  16905  setsid  17134  acsmapd  18477  intopsn  18579  cntzidss  19269  symggrp  19329  pmtrfv  19381  odmodnn0  19469  sylow2alem1  19546  telgsumfzs  19918  dprdsn  19967  dvdsrmul1  20305  dvrid  20342  cntzsubrng  20500  znunit  21518  isphld  21609  frlmup1  21753  evl1val  22273  evl1sca  22278  pf1const  22290  mat1f1o  22422  mat1mhm  22428  matunit  22622  pm2mpmhmlem2  22763  cctop  22950  iscnp4  23207  iscncl  23213  cnntr  23219  tx2cn  23554  xkoco1cn  23601  qtopkgen  23654  hmeontr  23713  hmeores  23715  filssufilg  23855  ustuqtop1  24185  utop2nei  24194  fmucndlem  24234  cfilufg  24236  xmetres2  24305  metres2  24307  metustto  24497  metust  24502  cfilucfil  24503  dscopn  24517  nmoi  24672  iccntr  24766  cphsqrtcl2  25142  cmsss  25307  ivthlem3  25410  sca2rab  25469  ovolicc2lem3  25476  mdegleb  26025  mdegmullem  26039  aalioulem3  26298  ulm2  26350  ulmcn  26364  root1eq1  26721  atanlogsublem  26881  birthdaylem3  26919  logexprlim  27192  dchrisumlem3  27458  f1otrg  28943  ax5seglem1  29001  ax5seglem2  29002  ax5seglem3a  29003  ax5seglem4  29005  ax5seglem9  29010  ax5seg  29011  axbtwnid  29012  axlowdimlem17  29031  axcontlem2  29038  axcontlem4  29040  axcontlem8  29044  cyclnumvtx  29873  rusgrnumwwlks  30050  wwlksext2clwwlk  30132  grpoidinv  30583  imsmetlem  30765  ipasslem1  30906  ip2eqi  30931  hvpncan  31114  pjid  31770  hmopre  31998  eigvalcl  32036  leopnmid  32213  superpos  32429  cvp  32450  rabfodom  32580  xlt2addrd  32839  hashxpe  32887  cyc3genpmlem  33233  lmodslmd  33286  elrgspnlem4  33327  elrgspnsubrunlem2  33330  nsgqusf1olem2  33495  elrspunidl  33509  prmidl0  33531  rsprprmprmidlb  33604  extdgfialglem1  33849  irngnminplynz  33869  constrfiss  33908  locfinreflem  33997  zarcls0  34025  fmcncfil  34088  rge0scvg  34106  esumfsup  34227  esumcvg  34243  insiga  34294  ballotlemirc  34689  signstfvcl  34730  signsvfn  34739  upgracycusgr  35349  subfacp1lem6  35379  satfdmlem  35562  msubff1  35750  fv2ndcnv  35972  matunitlindf  37819  ovoliunnfl  37863  voliunnfl  37865  volsupnfl  37866  ftc1anclem5  37898  indexa  37934  sstotbnd3  37977  heiborlem6  38017  rngosn3  38125  atlatmstc  39579  atlatle  39580  glbconN  39637  intnatN  39667  lnnat  39687  atcvrj2b  39692  atexchcvrN  39700  llncvrlpln  39818  lplncvrlvol  39876  lautcvr  40352  trlatn0  40432  cdleme48fvg  40760  cdlemg33c  40968  dihcl  41530  imadomfi  42256  fsuppssind  42836  elpell1qr2  43114  oddcomabszz  43186  wepwsolem  43284  mendring  43430  mendlmod  43431  hausgraph  43447  cantnftermord  43562  cantnfub  43563  cantnf2  43567  omabs2  43574  rp-isfinite5  43758  omelaxinf2  45230  cncmpmax  45277  eliinid  45355  icccncfext  46131  dvnprodlem2  46191  stoweidlem7  46251  stoweidlem34  46278  stoweidlem35  46279  stoweidlem59  46303  stoweidlem60  46304  stoweidlem62  46306  fourierdlem34  46385  fourierdlem73  46423  fourierdlem77  46427  etransclem35  46513  smfsuplem2  47056  pgrple2abl  48611  clddisj  49149