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  6140  ordin  6341  fimacnvdisj  6706  f1oexrnex  7867  wemoiso  7915  wemoiso2  7916  smocdmdom  8298  rdglim  8355  oaabs  8573  ecref  8677  f1oenfi  9103  f1oenfirn  9104  f1domfi  9105  domfi  9113  sdomdomtrfi  9125  php  9131  f1vrnfibi  9251  brwdom2  9484  infdiffi  9573  cantnflem1  9604  wemapwe  9612  cnfcom3lem  9618  r1lim  9687  carduni  9896  ac5num  9949  infunsdom1  10125  cofsmo  10182  isf32lem6  10271  hsmexlem1  10339  ac6c4  10394  fnct  10450  pwfseqlem1  10571  tskuni  10696  recgt1i  12041  avgle2  12384  eluzmn  12761  rpnnen1lem1  12898  xnn0le2is012  13167  fzneuz  13530  mulmod0  13800  hasheni  14274  hashun2  14309  hashf1dmrn  14369  reccn2  15523  isershft  15590  sumeq2ii  15619  prodeq2ii  15837  demoivreALT  16129  bitsp1  16361  gcdneg  16452  eucalginv  16514  eucalg  16517  odzdvds  16726  fldivp1  16828  prmunb  16845  vdwap1  16908  setsid  17137  acsmapd  18479  intopsn  18547  cntzidss  19238  symggrp  19298  pmtrfv  19350  odmodnn0  19438  sylow2alem1  19515  telgsumfzs  19887  dprdsn  19936  dvdsrmul1  20273  dvrid  20310  cntzsubrng  20471  znunit  21489  isphld  21580  frlmup1  21724  evl1val  22233  evl1sca  22238  pf1const  22250  mat1f1o  22382  mat1mhm  22388  matunit  22582  pm2mpmhmlem2  22723  cctop  22910  iscnp4  23167  iscncl  23173  cnntr  23179  tx2cn  23514  xkoco1cn  23561  qtopkgen  23614  hmeontr  23673  hmeores  23675  filssufilg  23815  ustuqtop1  24146  utop2nei  24155  fmucndlem  24195  cfilufg  24197  xmetres2  24266  metres2  24268  metustto  24458  metust  24463  cfilucfil  24464  dscopn  24478  nmoi  24633  iccntr  24727  cphsqrtcl2  25103  cmsss  25268  ivthlem3  25371  sca2rab  25430  ovolicc2lem3  25437  mdegleb  25986  mdegmullem  26000  aalioulem3  26259  ulm2  26311  ulmcn  26325  root1eq1  26682  atanlogsublem  26842  birthdaylem3  26880  logexprlim  27153  dchrisumlem3  27419  f1otrg  28835  ax5seglem1  28892  ax5seglem2  28893  ax5seglem3a  28894  ax5seglem4  28896  ax5seglem9  28901  ax5seg  28902  axbtwnid  28903  axlowdimlem17  28922  axcontlem2  28929  axcontlem4  28931  axcontlem8  28935  cyclnumvtx  29764  rusgrnumwwlks  29938  wwlksext2clwwlk  30020  grpoidinv  30471  imsmetlem  30653  ipasslem1  30794  ip2eqi  30819  hvpncan  31002  pjid  31658  hmopre  31886  eigvalcl  31924  leopnmid  32101  superpos  32317  cvp  32338  rabfodom  32468  xlt2addrd  32721  hashxpe  32771  cyc3genpmlem  33112  lmodslmd  33165  elrgspnlem4  33204  elrgspnsubrunlem2  33207  nsgqusf1olem2  33370  elrspunidl  33384  prmidl0  33406  rsprprmprmidlb  33479  extdgfialglem1  33678  irngnminplynz  33698  constrfiss  33737  locfinreflem  33826  zarcls0  33854  fmcncfil  33917  rge0scvg  33935  esumfsup  34056  esumcvg  34072  insiga  34123  ballotlemirc  34519  signstfvcl  34560  signsvfn  34569  upgracycusgr  35147  subfacp1lem6  35177  satfdmlem  35360  msubff1  35548  fv2ndcnv  35770  matunitlindf  37617  ovoliunnfl  37661  voliunnfl  37663  volsupnfl  37664  ftc1anclem5  37696  indexa  37732  sstotbnd3  37775  heiborlem6  37815  rngosn3  37923  atlatmstc  39317  atlatle  39318  glbconN  39375  glbconNOLD  39376  intnatN  39406  lnnat  39426  atcvrj2b  39431  atexchcvrN  39439  llncvrlpln  39557  lplncvrlvol  39615  lautcvr  40091  trlatn0  40171  cdleme48fvg  40499  cdlemg33c  40707  dihcl  41269  imadomfi  41995  fsuppssind  42586  elpell1qr2  42865  oddcomabszz  42937  wepwsolem  43035  mendring  43181  mendlmod  43182  hausgraph  43198  cantnftermord  43313  cantnfub  43314  cantnf2  43318  omabs2  43325  rp-isfinite5  43510  omelaxinf2  44983  cncmpmax  45030  eliinid  45109  icccncfext  45888  dvnprodlem2  45948  stoweidlem7  46008  stoweidlem34  46035  stoweidlem35  46036  stoweidlem59  46060  stoweidlem60  46061  stoweidlem62  46063  fourierdlem34  46142  fourierdlem73  46180  fourierdlem77  46184  etransclem35  46270  smfsuplem2  46813  pgrple2abl  48369  clddisj  48908