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

Syntax hints:   → wi 4   ∧ wa 396

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 206  df-an 397

This theorem is referenced by:  sofld  6186  ordin  6394  fimacnvdisj  6769  f1oexrnex  7920  wemoiso  7962  wemoiso2  7963  smocdmdom  8370  rdglim  8428  oaabs  8649  ssctOLD  9054  f1oenfi  9184  f1oenfirn  9185  f1domfi  9186  domfi  9194  sdomdomtrfi  9206  php  9212  onomeneqOLD  9231  f1vrnfibi  9339  brwdom2  9570  infdiffi  9655  cantnflem1  9686  wemapwe  9694  cnfcom3lem  9700  r1lim  9769  carduni  9978  ac5num  10033  infunsdom1  10210  cofsmo  10266  isf32lem6  10355  hsmexlem1  10423  ac6c4  10478  fnct  10534  pwfseqlem1  10655  tskuni  10780  recgt1i  12113  avgle2  12455  eluzmn  12831  rpnnen1lem1  12964  xnn0le2is012  13227  fzneuz  13584  mulmod0  13844  hasheni  14310  hashun2  14345  hashf1dmrn  14405  reccn2  15543  isershft  15612  sumeq2ii  15641  prodeq2ii  15859  demoivreALT  16146  bitsp1  16374  gcdneg  16465  eucalginv  16523  eucalg  16526  odzdvds  16730  fldivp1  16832  prmunb  16849  vdwap1  16912  setsid  17143  acsmapd  18509  intopsn  18575  cntzidss  19206  symggrp  19270  pmtrfv  19322  odmodnn0  19410  sylow2alem1  19487  telgsumfzs  19859  dprdsn  19908  dvdsrmul1  20187  dvrid  20224  znunit  21125  isphld  21213  frlmup1  21359  evl1val  21855  evl1sca  21860  pf1const  21872  mat1f1o  21987  mat1mhm  21993  matunit  22187  pm2mpmhmlem2  22328  cctop  22516  iscnp4  22774  iscncl  22780  cnntr  22786  tx2cn  23121  xkoco1cn  23168  qtopkgen  23221  hmeontr  23280  hmeores  23282  filssufilg  23422  ustuqtop1  23753  utop2nei  23762  fmucndlem  23803  cfilufg  23805  xmetres2  23874  metres2  23876  metustto  24069  metust  24074  cfilucfil  24075  dscopn  24089  nmoi  24252  iccntr  24344  cphsqrtcl2  24710  cmsss  24875  ivthlem3  24977  sca2rab  25036  ovolicc2lem3  25043  mdegleb  25589  mdegmullem  25603  aalioulem3  25854  ulm2  25904  ulmcn  25918  root1eq1  26270  atanlogsublem  26427  birthdaylem3  26465  logexprlim  26735  dchrisumlem3  27001  f1otrg  28160  ax5seglem1  28224  ax5seglem2  28225  ax5seglem3a  28226  ax5seglem4  28228  ax5seglem9  28233  ax5seg  28234  axbtwnid  28235  axlowdimlem17  28254  axcontlem2  28261  axcontlem4  28263  axcontlem8  28267  rusgrnumwwlks  29266  wwlksext2clwwlk  29348  grpoidinv  29799  imsmetlem  29981  ipasslem1  30122  ip2eqi  30147  hvpncan  30330  pjid  30986  hmopre  31214  eigvalcl  31252  leopnmid  31429  superpos  31645  cvp  31666  rabfodom  31781  ecref  31971  xlt2addrd  32009  hashxpe  32057  cyc3genpmlem  32351  lmodslmd  32390  nsgqusf1olem2  32570  elrspunidl  32591  prmidl0  32614  irngnminplynz  32831  locfinreflem  32889  zarcls0  32917  fmcncfil  32980  rge0scvg  32998  esumfsup  33137  esumcvg  33153  insiga  33204  ballotlemirc  33599  signstfvcl  33653  signsvfn  33662  upgracycusgr  34215  subfacp1lem6  34245  satfdmlem  34428  msubff1  34616  fv2ndcnv  34818  matunitlindf  36572  ovoliunnfl  36616  voliunnfl  36618  volsupnfl  36619  ftc1anclem5  36651  indexa  36687  sstotbnd3  36730  heiborlem6  36770  rngosn3  36878  atlatmstc  38275  atlatle  38276  glbconN  38333  glbconNOLD  38334  intnatN  38364  lnnat  38384  atcvrj2b  38389  atexchcvrN  38397  llncvrlpln  38515  lplncvrlvol  38573  lautcvr  39049  trlatn0  39129  cdleme48fvg  39457  cdlemg33c  39665  dihcl  40227  fsuppssind  41247  elpell1qr2  41692  oddcomabszz  41765  wepwsolem  41866  mendring  42016  mendlmod  42017  hausgraph  42036  cantnftermord  42152  cantnfub  42153  cantnf2  42157  omabs2  42164  rp-isfinite5  42350  cncmpmax  43798  eliinid  43882  icccncfext  44682  dvnprodlem2  44742  stoweidlem7  44802  stoweidlem34  44829  stoweidlem35  44830  stoweidlem59  44854  stoweidlem60  44855  stoweidlem62  44857  fourierdlem34  44936  fourierdlem73  44974  fourierdlem77  44978  etransclem35  45064  smfsuplem2  45607  cntzsubrng  46825  pgrple2abl  47120  clddisj  47614