Theorem sylancom 600

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  sofld  6178  ordin  6393  fimacnvdisj  6761  f1oexrnex  7940  wemoiso  7986  wemoiso2  7987  smocdmdom  8380  rdglim  8438  oaabs  8661  ecref  8767  f1oenfi  9198  f1oenfirn  9199  f1domfi  9200  domfi  9208  sdomdomtrfi  9220  php  9226  f1vrnfibi  9335  brwdom2  9571  infdiffi  9663  cantnflem1  9694  wemapwe  9702  cnfcom3lem  9708  r1lim  9783  carduni  10066  ac5num  10119  infunsdom1  10294  cofsmo  10351  isf32lem6  10440  hsmexlem1  10508  ac6c4  10563  fnct  10624  fnctOLD  10625  pwfseqlem1  10747  tskuni  10872  recgt1i  12218  avgle2  12591  eluzmn  12976  rpnnen1lem1  13110  xnn0le2is012  13380  fzneuz  13746  mulmod0  14021  hasheni  14496  hashun2  14531  hashf1dmrn  14592  reccn2  15770  isershft  15837  sumeq2ii  15866  prodeq2ii  16086  demoivreALT  16375  bitsp1  16607  gcdneg  16700  eucalginv  16765  eucalg  16768  odzdvds  16979  fldivp1  17081  prmunb  17098  vdwap1  17161  setsid  17391  acsmapd  18734  intopsn  18838  cntzidss  19560  symggrp  19620  pmtrfv  19672  odmodnn0  19760  sylow2alem1  19837  telgsumfzs  20209  dprdsn  20258  dvdsrmul1  20605  dvrid  20642  cntzsubrng  20825  prmidl0  21640  znunit  21875  isphld  21966  frlmup1  22110  evl1val  22653  evl1sca  22658  pf1const  22670  mat1f1o  22799  mat1mhm  22805  matunit  22999  matunitlindf  23002  pm2mpmhmlem2  23143  cctop  23330  iscnp4  23587  iscncl  23593  cnntr  23599  tx2cn  23935  xkoco1cn  23982  qtopkgen  24035  hmeontr  24094  hmeores  24096  filssufilg  24236  ustuqtop1  24566  utop2nei  24575  fmucndlem  24615  cfilufg  24617  xmetres2  24686  metres2  24688  metustto  24878  metust  24883  cfilucfil  24884  dscopn  24898  nmoi  25053  iccntr  25147  cphsqrtcl2  25513  cmsss  25678  ivthlem3  25780  sca2rab  25839  ovolicc2lem3  25846  mdegleb  26388  mdegmullem  26402  aalioulem3  26667  ulm2  26718  ulmcn  26732  root1eq1  27089  atanlogsublem  27249  birthdaylem3  27287  logexprlim  27558  dchrisumlem3  27824  f1otrg  29454  ax5seglem1  29512  ax5seglem2  29513  ax5seglem3a  29514  ax5seglem4  29516  ax5seglem9  29521  ax5seg  29522  axbtwnid  29523  axlowdimlem17  29542  axcontlem2  29549  axcontlem4  29551  axcontlem8  29555  cyclnumvtx  30394  rusgrnumwwlks  30572  wwlksext2clwwlk  30654  grpoidinv  31116  imsmetlem  31298  ipasslem1  31439  ip2eqi  31464  hvpncan  31647  pjid  32303  hmopre  32531  eigvalcl  32569  leopnmid  32746  superpos  32962  cvp  32983  rabfodom  33149  xlt2addrd  33398  hashxpe  33446  suppgsumssiun  33680  cyc3genpmlem  33759  lmodslmd  33812  elrgspnlem4  33853  elrgspnsubrunlem2  33856  nsgqusf1olem2  34012  elrspunidl  34025  rsprprmprmidlb  34102  extdgfialglem1  34371  irngnminplynz  34391  constrfiss  34430  reff  34518  locfinreflem  34519  zarcls0  34547  fmcncfil  34610  rge0scvg  34628  esumfsup  34749  esumcvg  34765  insiga  34817  ballotlemirc  35211  signstfvcl  35249  signsvfn  35258  upgracycusgr  35997  subfacp1lem6  36037  satfdmlem  36220  msubff1  36408  fv2ndcnv  36635  ovoliunnfl  38674  voliunnfl  38676  volsupnfl  38677  ftc1anclem5  38709  indexa  38761  sstotbnd3  38804  heiborlem6  38844  rngosn3  38952  atlatmstc  40470  atlatle  40471  glbconN  40528  intnatN  40558  lnnat  40578  atcvrj2b  40583  atexchcvrN  40591  llncvrlpln  40709  lplncvrlvol  40767  lautcvr  41243  trlatn0  41323  cdleme48fvg  41651  cdlemg33c  41859  dihcl  42421  imadomfi  43146  fsuppssind  43715  elpell1qr2  43973  oddcomabszz  44045  wepwsolem  44143  mendring  44284  mendlmod  44285  hausgraph  44301  cantnftermord  44416  cantnfub  44417  cantnf2  44421  omabs2  44428  rp-isfinite5  44612  omelaxinf2  46073  cncmpmax  46143  eliinid  46220  icccncfext  46991  dvnprodlem2  47051  stoweidlem7  47111  stoweidlem34  47138  stoweidlem35  47139  stoweidlem59  47163  stoweidlem60  47164  stoweidlem62  47166  fourierdlem34  47245  fourierdlem73  47283  fourierdlem77  47287  etransclem35  47373  smfsuplem2  47916  pgrple2abl  49571  clddisj  50112  veroquadgsumlem  51152