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  6183  ordin  6391  fimacnvdisj  6766  f1oexrnex  7914  wemoiso  7956  wemoiso2  7957  smocdmdom  8364  rdglim  8422  oaabs  8643  ssctOLD  9048  f1oenfi  9178  f1oenfirn  9179  f1domfi  9180  domfi  9188  sdomdomtrfi  9200  php  9206  onomeneqOLD  9225  f1vrnfibi  9333  brwdom2  9564  infdiffi  9649  cantnflem1  9680  wemapwe  9688  cnfcom3lem  9694  r1lim  9763  carduni  9972  ac5num  10027  infunsdom1  10204  cofsmo  10260  isf32lem6  10349  hsmexlem1  10417  ac6c4  10472  fnct  10528  pwfseqlem1  10649  tskuni  10774  recgt1i  12107  avgle2  12449  eluzmn  12825  rpnnen1lem1  12958  xnn0le2is012  13221  fzneuz  13578  mulmod0  13838  hasheni  14304  hashun2  14339  hashf1dmrn  14399  reccn2  15537  isershft  15606  sumeq2ii  15635  prodeq2ii  15853  demoivreALT  16140  bitsp1  16368  gcdneg  16459  eucalginv  16517  eucalg  16520  odzdvds  16724  fldivp1  16826  prmunb  16843  vdwap1  16906  setsid  17137  acsmapd  18503  intopsn  18569  cntzidss  19198  symggrp  19262  pmtrfv  19314  odmodnn0  19402  sylow2alem1  19479  telgsumfzs  19851  dprdsn  19900  dvdsrmul1  20175  dvrid  20212  znunit  21110  isphld  21198  frlmup1  21344  evl1val  21839  evl1sca  21844  pf1const  21856  mat1f1o  21971  mat1mhm  21977  matunit  22171  pm2mpmhmlem2  22312  cctop  22500  iscnp4  22758  iscncl  22764  cnntr  22770  tx2cn  23105  xkoco1cn  23152  qtopkgen  23205  hmeontr  23264  hmeores  23266  filssufilg  23406  ustuqtop1  23737  utop2nei  23746  fmucndlem  23787  cfilufg  23789  xmetres2  23858  metres2  23860  metustto  24053  metust  24058  cfilucfil  24059  dscopn  24073  nmoi  24236  iccntr  24328  cphsqrtcl2  24694  cmsss  24859  ivthlem3  24961  sca2rab  25020  ovolicc2lem3  25027  mdegleb  25573  mdegmullem  25587  aalioulem3  25838  ulm2  25888  ulmcn  25902  root1eq1  26252  atanlogsublem  26409  birthdaylem3  26447  logexprlim  26717  dchrisumlem3  26983  f1otrg  28111  ax5seglem1  28175  ax5seglem2  28176  ax5seglem3a  28177  ax5seglem4  28179  ax5seglem9  28184  ax5seg  28185  axbtwnid  28186  axlowdimlem17  28205  axcontlem2  28212  axcontlem4  28214  axcontlem8  28218  rusgrnumwwlks  29217  wwlksext2clwwlk  29299  grpoidinv  29748  imsmetlem  29930  ipasslem1  30071  ip2eqi  30096  hvpncan  30279  pjid  30935  hmopre  31163  eigvalcl  31201  leopnmid  31378  superpos  31594  cvp  31615  rabfodom  31730  ecref  31920  xlt2addrd  31958  hashxpe  32006  cyc3genpmlem  32297  lmodslmd  32336  nsgqusf1olem2  32513  elrspunidl  32534  prmidl0  32557  irngnminplynz  32759  locfinreflem  32808  zarcls0  32836  fmcncfil  32899  rge0scvg  32917  esumfsup  33056  esumcvg  33072  insiga  33123  ballotlemirc  33518  signstfvcl  33572  signsvfn  33581  upgracycusgr  34134  subfacp1lem6  34164  satfdmlem  34347  msubff1  34535  fv2ndcnv  34737  matunitlindf  36474  ovoliunnfl  36518  voliunnfl  36520  volsupnfl  36521  ftc1anclem5  36553  indexa  36589  sstotbnd3  36632  heiborlem6  36672  rngosn3  36780  atlatmstc  38177  atlatle  38178  glbconN  38235  glbconNOLD  38236  intnatN  38266  lnnat  38286  atcvrj2b  38291  atexchcvrN  38299  llncvrlpln  38417  lplncvrlvol  38475  lautcvr  38951  trlatn0  39031  cdleme48fvg  39359  cdlemg33c  39567  dihcl  40129  fsuppssind  41162  elpell1qr2  41595  oddcomabszz  41668  wepwsolem  41769  mendring  41919  mendlmod  41920  hausgraph  41939  cantnftermord  42055  cantnfub  42056  cantnf2  42060  omabs2  42067  rp-isfinite5  42253  cncmpmax  43701  eliinid  43785  icccncfext  44589  dvnprodlem2  44649  stoweidlem7  44709  stoweidlem34  44736  stoweidlem35  44737  stoweidlem59  44761  stoweidlem60  44762  stoweidlem62  44764  fourierdlem34  44843  fourierdlem73  44881  fourierdlem77  44885  etransclem35  44971  smfsuplem2  45514  cntzsubrng  46730  pgrple2abl  46994  clddisj  47489