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  6160  ordin  6362  fimacnvdisj  6738  f1oexrnex  7903  wemoiso  7952  wemoiso2  7953  smocdmdom  8337  rdglim  8394  oaabs  8612  ecref  8716  f1oenfi  9143  f1oenfirn  9144  f1domfi  9145  domfi  9153  sdomdomtrfi  9165  php  9171  f1vrnfibi  9293  brwdom2  9526  infdiffi  9611  cantnflem1  9642  wemapwe  9650  cnfcom3lem  9656  r1lim  9725  carduni  9934  ac5num  9989  infunsdom1  10165  cofsmo  10222  isf32lem6  10311  hsmexlem1  10379  ac6c4  10434  fnct  10490  pwfseqlem1  10611  tskuni  10736  recgt1i  12080  avgle2  12423  eluzmn  12800  rpnnen1lem1  12937  xnn0le2is012  13206  fzneuz  13569  mulmod0  13839  hasheni  14313  hashun2  14348  hashf1dmrn  14408  reccn2  15563  isershft  15630  sumeq2ii  15659  prodeq2ii  15877  demoivreALT  16169  bitsp1  16401  gcdneg  16492  eucalginv  16554  eucalg  16557  odzdvds  16766  fldivp1  16868  prmunb  16885  vdwap1  16948  setsid  17177  acsmapd  18513  intopsn  18581  cntzidss  19272  symggrp  19330  pmtrfv  19382  odmodnn0  19470  sylow2alem1  19547  telgsumfzs  19919  dprdsn  19968  dvdsrmul1  20278  dvrid  20315  cntzsubrng  20476  znunit  21473  isphld  21563  frlmup1  21707  evl1val  22216  evl1sca  22221  pf1const  22233  mat1f1o  22365  mat1mhm  22371  matunit  22565  pm2mpmhmlem2  22706  cctop  22893  iscnp4  23150  iscncl  23156  cnntr  23162  tx2cn  23497  xkoco1cn  23544  qtopkgen  23597  hmeontr  23656  hmeores  23658  filssufilg  23798  ustuqtop1  24129  utop2nei  24138  fmucndlem  24178  cfilufg  24180  xmetres2  24249  metres2  24251  metustto  24441  metust  24446  cfilucfil  24447  dscopn  24461  nmoi  24616  iccntr  24710  cphsqrtcl2  25086  cmsss  25251  ivthlem3  25354  sca2rab  25413  ovolicc2lem3  25420  mdegleb  25969  mdegmullem  25983  aalioulem3  26242  ulm2  26294  ulmcn  26308  root1eq1  26665  atanlogsublem  26825  birthdaylem3  26863  logexprlim  27136  dchrisumlem3  27402  f1otrg  28798  ax5seglem1  28855  ax5seglem2  28856  ax5seglem3a  28857  ax5seglem4  28859  ax5seglem9  28864  ax5seg  28865  axbtwnid  28866  axlowdimlem17  28885  axcontlem2  28892  axcontlem4  28894  axcontlem8  28898  cyclnumvtx  29730  rusgrnumwwlks  29904  wwlksext2clwwlk  29986  grpoidinv  30437  imsmetlem  30619  ipasslem1  30760  ip2eqi  30785  hvpncan  30968  pjid  31624  hmopre  31852  eigvalcl  31890  leopnmid  32067  superpos  32283  cvp  32304  rabfodom  32434  xlt2addrd  32682  hashxpe  32732  cyc3genpmlem  33108  lmodslmd  33157  elrgspnlem4  33196  elrgspnsubrunlem2  33199  nsgqusf1olem2  33385  elrspunidl  33399  prmidl0  33421  rsprprmprmidlb  33494  irngnminplynz  33702  constrfiss  33741  locfinreflem  33830  zarcls0  33858  fmcncfil  33921  rge0scvg  33939  esumfsup  34060  esumcvg  34076  insiga  34127  ballotlemirc  34523  signstfvcl  34564  signsvfn  34573  upgracycusgr  35142  subfacp1lem6  35172  satfdmlem  35355  msubff1  35543  fv2ndcnv  35765  matunitlindf  37612  ovoliunnfl  37656  voliunnfl  37658  volsupnfl  37659  ftc1anclem5  37691  indexa  37727  sstotbnd3  37770  heiborlem6  37810  rngosn3  37918  atlatmstc  39312  atlatle  39313  glbconN  39370  glbconNOLD  39371  intnatN  39401  lnnat  39421  atcvrj2b  39426  atexchcvrN  39434  llncvrlpln  39552  lplncvrlvol  39610  lautcvr  40086  trlatn0  40166  cdleme48fvg  40494  cdlemg33c  40702  dihcl  41264  imadomfi  41990  fsuppssind  42581  elpell1qr2  42860  oddcomabszz  42933  wepwsolem  43031  mendring  43177  mendlmod  43178  hausgraph  43194  cantnftermord  43309  cantnfub  43310  cantnf2  43314  omabs2  43321  rp-isfinite5  43506  omelaxinf2  44979  cncmpmax  45026  eliinid  45105  icccncfext  45885  dvnprodlem2  45945  stoweidlem7  46005  stoweidlem34  46032  stoweidlem35  46033  stoweidlem59  46057  stoweidlem60  46058  stoweidlem62  46060  fourierdlem34  46139  fourierdlem73  46177  fourierdlem77  46181  etransclem35  46267  smfsuplem2  46810  pgrple2abl  48353  clddisj  48892