Theorem sylancom 599

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

Syntax hints:   → wi 4   ∧ wa 400

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 210  df-an 401

This theorem is referenced by:  sofld  6184  ordin  6388  fimacnvdisj  6754  f1oexrnex  7920  wemoiso  7966  wemoiso2  7967  smocdmdom  8351  rdglim  8409  oaabs  8630  ecref  8736  f1oenfi  9159  f1oenfirn  9160  f1domfi  9161  domfi  9169  sdomdomtrfi  9181  php  9187  f1vrnfibi  9295  brwdom2  9531  infdiffi  9623  cantnflem1  9654  wemapwe  9662  cnfcom3lem  9668  r1lim  9740  carduni  9963  ac5num  10016  infunsdom1  10191  cofsmo  10249  isf32lem6  10338  hsmexlem1  10406  ac6c4  10461  fnct  10517  pwfseqlem1  10639  tskuni  10764  recgt1i  12108  avgle2  12481  eluzmn  12865  rpnnen1lem1  12998  xnn0le2is012  13268  fzneuz  13632  mulmod0  13906  hasheni  14380  hashun2  14415  hashf1dmrn  14476  reccn2  15644  isershft  15711  sumeq2ii  15740  prodeq2ii  15961  demoivreALT  16253  bitsp1  16485  gcdneg  16576  eucalginv  16638  eucalg  16641  odzdvds  16851  fldivp1  16953  prmunb  16970  vdwap1  17033  setsid  17263  acsmapd  18606  intopsn  18708  cntzidss  19406  symggrp  19466  pmtrfv  19518  odmodnn0  19606  sylow2alem1  19683  telgsumfzs  20055  dprdsn  20104  dvdsrmul1  20447  dvrid  20484  cntzsubrng  20648  prmidl0  21443  znunit  21678  isphld  21769  frlmup1  21913  evl1val  22454  evl1sca  22459  pf1const  22471  mat1f1o  22600  mat1mhm  22606  matunit  22800  pm2mpmhmlem2  22941  cctop  23128  iscnp4  23385  iscncl  23391  cnntr  23397  tx2cn  23732  xkoco1cn  23779  qtopkgen  23832  hmeontr  23891  hmeores  23893  filssufilg  24033  ustuqtop1  24363  utop2nei  24372  fmucndlem  24412  cfilufg  24414  xmetres2  24483  metres2  24485  metustto  24675  metust  24680  cfilucfil  24681  dscopn  24695  nmoi  24850  iccntr  24944  cphsqrtcl2  25310  cmsss  25475  ivthlem3  25577  sca2rab  25636  ovolicc2lem3  25643  mdegleb  26186  mdegmullem  26200  aalioulem3  26460  ulm2  26510  ulmcn  26524  root1eq1  26882  atanlogsublem  27042  birthdaylem3  27080  logexprlim  27351  dchrisumlem3  27617  f1otrg  29157  ax5seglem1  29215  ax5seglem2  29216  ax5seglem3a  29217  ax5seglem4  29219  ax5seglem9  29224  ax5seg  29225  axbtwnid  29226  axlowdimlem17  29245  axcontlem2  29252  axcontlem4  29254  axcontlem8  29258  cyclnumvtx  30086  rusgrnumwwlks  30263  wwlksext2clwwlk  30345  grpoidinv  30797  imsmetlem  30979  ipasslem1  31120  ip2eqi  31145  hvpncan  31328  pjid  31984  hmopre  32212  eigvalcl  32250  leopnmid  32427  superpos  32643  cvp  32664  rabfodom  32788  xlt2addrd  33041  hashxpe  33089  suppgsumssiun  33329  cyc3genpmlem  33408  lmodslmd  33461  elrgspnlem4  33502  elrgspnsubrunlem2  33505  nsgqusf1olem2  33663  elrspunidl  33676  rsprprmprmidlb  33754  extdgfialglem1  34023  irngnminplynz  34043  constrfiss  34082  locfinreflem  34171  zarcls0  34199  fmcncfil  34262  rge0scvg  34280  esumfsup  34401  esumcvg  34417  insiga  34468  ballotlemirc  34863  signstfvcl  34901  signsvfn  34910  upgracycusgr  35542  subfacp1lem6  35572  satfdmlem  35755  msubff1  35943  fv2ndcnv  36165  matunitlindf  38152  ovoliunnfl  38196  voliunnfl  38198  volsupnfl  38199  ftc1anclem5  38231  indexa  38267  sstotbnd3  38310  heiborlem6  38350  rngosn3  38458  atlatmstc  39978  atlatle  39979  glbconN  40036  intnatN  40066  lnnat  40086  atcvrj2b  40091  atexchcvrN  40099  llncvrlpln  40217  lplncvrlvol  40275  lautcvr  40751  trlatn0  40831  cdleme48fvg  41159  cdlemg33c  41367  dihcl  41929  imadomfi  42654  fsuppssind  43210  elpell1qr2  43484  oddcomabszz  43556  wepwsolem  43654  mendring  43800  mendlmod  43801  hausgraph  43817  cantnftermord  43932  cantnfub  43933  cantnf2  43937  omabs2  43944  rp-isfinite5  44128  omelaxinf2  45583  cncmpmax  45637  eliinid  45714  icccncfext  46486  dvnprodlem2  46546  stoweidlem7  46606  stoweidlem34  46633  stoweidlem35  46634  stoweidlem59  46658  stoweidlem60  46659  stoweidlem62  46661  fourierdlem34  46740  fourierdlem73  46778  fourierdlem77  46782  etransclem35  46868  smfsuplem2  47411  pgrple2abl  49023  clddisj  49560