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

This theorem is referenced by:  sofld  5920  ordin  6096  fimacnvdisj  6425  f1oexrnex  7488  wemoiso  7530  wemoiso2  7531  smorndom  7857  rdglim  7914  oaabs  8121  ssct  8445  onomeneq  8554  domfi  8585  f1vrnfibi  8655  brwdom2  8883  infdiffi  8967  cantnflem1  8998  wemapwe  9006  cnfcom3lem  9012  r1lim  9047  carduni  9256  ac5num  9308  infunsdom1  9481  cofsmo  9537  isf32lem6  9626  hsmexlem1  9694  ac6c4  9749  fnct  9805  pwfseqlem1  9926  tskuni  10051  recgt1i  11385  avgle2  11726  eluzmn  12100  rpnnen1lem1  12227  xnn0le2is012  12489  fzneuz  12838  mulmod0  13095  hasheni  13558  hashun2  13592  swrdccatin1  13923  reccn2  14787  isershft  14854  sumeq2ii  14883  prodeq2ii  15100  demoivreALT  15387  bitsp1  15613  gcdneg  15703  eucalginv  15757  eucalg  15760  odzdvds  15961  fldivp1  16062  prmunb  16079  vdwap1  16142  setsid  16367  acsmapd  17617  intopsn  17692  cntzidss  18209  symggrp  18259  pmtrfv  18311  odmodnn0  18399  sylow2alem1  18472  telgsumfzs  18826  dprdsn  18875  dvdsrmul1  19093  dvrid  19128  evl1val  20174  evl1sca  20179  pf1const  20191  znunit  20392  isphld  20480  frlmup1  20624  mat1f1o  20771  mat1mhm  20777  matunit  20971  pm2mpmhmlem2  21111  cctop  21298  iscnp4  21555  iscncl  21561  cnntr  21567  tx2cn  21902  xkoco1cn  21949  qtopkgen  22002  hmeontr  22061  hmeores  22063  filssufilg  22203  ustuqtop1  22533  utop2nei  22542  fmucndlem  22583  cfilufg  22585  xmetres2  22654  metres2  22656  metustto  22846  metust  22851  cfilucfil  22852  dscopn  22866  nmoi  23020  iccntr  23112  cphsqrtcl2  23473  cmsss  23637  ivthlem3  23737  sca2rab  23796  ovolicc2lem3  23803  mdegleb  24341  aalioulem3  24606  ulm2  24656  ulmcn  24670  root1eq1  25017  atanlogsublem  25174  birthdaylem3  25213  logexprlim  25483  dchrisumlem3  25749  f1otrg  26340  ax5seglem1  26397  ax5seglem2  26398  ax5seglem3a  26399  ax5seglem4  26401  ax5seglem9  26406  ax5seg  26407  axbtwnid  26408  axlowdimlem17  26427  axcontlem2  26434  axcontlem4  26436  axcontlem8  26440  rusgrnumwwlks  27440  grpoidinv  27976  imsmetlem  28158  ipasslem1  28299  ip2eqi  28324  hvpncan  28507  pjid  29163  hmopre  29391  eigvalcl  29429  leopnmid  29606  superpos  29822  cvp  29843  rabfodom  29958  xlt2addrd  30170  hashxpe  30213  cyc3genpmlem  30431  lmodslmd  30470  locfinreflem  30721  fmcncfil  30791  rge0scvg  30809  esumfsup  30946  esumcvg  30962  insiga  31013  ballotlemirc  31406  signstfvcl  31460  hashf1dmrn  31969  upgracycusgr  32010  subfacp1lem6  32040  satfdmlem  32223  msubff1  32411  fv2ndcnv  32629  matunitlindf  34421  ovoliunnfl  34465  voliunnfl  34467  volsupnfl  34468  ftc1anclem5  34502  indexa  34540  sstotbnd3  34586  heiborlem6  34626  rngosn3  34734  atlatmstc  35986  atlatle  35987  glbconN  36044  intnatN  36074  lnnat  36094  atcvrj2b  36099  atexchcvrN  36107  llncvrlpln  36225  lplncvrlvol  36283  lautcvr  36759  trlatn0  36839  cdleme48fvg  37167  cdlemg33c  37375  dihcl  37937  elpell1qr2  38954  oddcomabszz  39026  wepwsolem  39127  mendring  39277  mendlmod  39278  hausgraph  39297  rp-isfinite5  39368  cncmpmax  40828  eliinid  40917  icccncfext  41711  dvnprodlem2  41773  stoweidlem7  41834  stoweidlem34  41861  stoweidlem35  41862  stoweidlem59  41886  stoweidlem60  41887  stoweidlem62  41889  fourierdlem34  41968  fourierdlem73  42006  fourierdlem77  42010  etransclem35  42096  smfsuplem2  42628  pgrple2abl  43893