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  6197  ordin  6419  fimacnvdisj  6790  f1oexrnex  7973  wemoiso  8019  wemoiso2  8020  smocdmdom  8414  rdglim  8472  oaabs  8695  ecref  8801  f1oenfi  9232  f1oenfirn  9233  f1domfi  9234  domfi  9242  sdomdomtrfi  9254  php  9260  f1vrnfibi  9369  brwdom2  9604  infdiffi  9696  cantnflem1  9727  wemapwe  9735  cnfcom3lem  9741  r1lim  9816  carduni  10101  ac5num  10154  infunsdom1  10329  cofsmo  10386  isf32lem6  10475  hsmexlem1  10543  ac6c4  10598  fnct  10659  fnctOLD  10660  pwfseqlem1  10782  tskuni  10907  recgt1i  12254  avgle2  12627  eluzmn  13012  rpnnen1lem1  13146  xnn0le2is012  13416  fzneuz  13782  mulmod0  14057  hasheni  14533  hashun2  14568  hashf1dmrn  14629  reccn2  15808  isershft  15875  sumeq2ii  15904  prodeq2ii  16124  demoivreALT  16413  bitsp1  16645  gcdneg  16738  eucalginv  16803  eucalg  16806  odzdvds  17017  fldivp1  17119  prmunb  17136  vdwap1  17199  setsid  17429  acsmapd  18778  intopsn  18882  cntzidss  19605  symggrp  19665  pmtrfv  19717  odmodnn0  19805  sylow2alem1  19882  telgsumfzs  20254  dprdsn  20303  dvdsrmul1  20650  dvrid  20687  cntzsubrng  20870  prmidl0  21685  znunit  21924  isphld  22015  frlmup1  22159  evl1val  22702  evl1sca  22707  pf1const  22719  mat1f1o  22848  mat1mhm  22854  matunit  23048  matunitlindf  23051  pm2mpmhmlem2  23192  cctop  23379  iscnp4  23636  iscncl  23642  cnntr  23648  tx2cn  23984  xkoco1cn  24031  qtopkgen  24084  hmeontr  24143  hmeores  24145  filssufilg  24285  ustuqtop1  24615  utop2nei  24624  fmucndlem  24664  cfilufg  24666  xmetres2  24735  metres2  24737  metustto  24927  metust  24932  cfilucfil  24933  dscopn  24947  nmoi  25102  iccntr  25196  cphsqrtcl2  25562  cmsss  25727  ivthlem3  25829  sca2rab  25888  ovolicc2lem3  25895  mdegleb  26437  mdegmullem  26451  aalioulem3  26718  ulm2  26769  ulmcn  26783  root1eq1  27140  atanlogsublem  27300  birthdaylem3  27338  logexprlim  27609  dchrisumlem3  27875  f1otrg  29505  ax5seglem1  29563  ax5seglem2  29564  ax5seglem3a  29565  ax5seglem4  29567  ax5seglem9  29572  ax5seg  29573  axbtwnid  29574  axlowdimlem17  29593  axcontlem2  29600  axcontlem4  29602  axcontlem8  29606  cyclnumvtx  30445  rusgrnumwwlks  30623  wwlksext2clwwlk  30705  grpoidinv  31167  imsmetlem  31349  ipasslem1  31490  ip2eqi  31515  hvpncan  31698  pjid  32354  hmopre  32582  eigvalcl  32620  leopnmid  32797  superpos  33013  cvp  33034  rabfodom  33200  xlt2addrd  33447  hashxpe  33495  suppgsumssiun  33732  cyc3genpmlem  33811  lmodslmd  33864  elrgspnlem4  33905  elrgspnsubrunlem2  33908  nsgqusf1olem2  34069  elrspunidl  34082  rsprprmprmidlb  34159  extdgfialglem1  34435  irngnminplynz  34455  constrfiss  34494  reff  34582  locfinreflem  34583  zarcls0  34611  fmcncfil  34674  rge0scvg  34692  esumfsup  34813  esumcvg  34829  insiga  34881  ballotlemirc  35275  signstfvcl  35313  signsvfn  35322  upgracycusgr  36118  subfacp1lem6  36158  satfdmlem  36341  msubff1  36529  fv2ndcnv  36757  ovoliunnfl  38848  voliunnfl  38850  volsupnfl  38851  ftc1anclem5  38883  indexa  38935  sstotbnd3  38976  heiborlem6  39016  rngosn3  39124  atlatmstc  40642  atlatle  40643  glbconN  40700  intnatN  40730  lnnat  40750  atcvrj2b  40755  atexchcvrN  40763  llncvrlpln  40881  lplncvrlvol  40939  lautcvr  41415  trlatn0  41495  cdleme48fvg  41823  cdlemg33c  42031  dihcl  42593  imadomfi  43318  fsuppssind  43887  elpell1qr2  44145  oddcomabszz  44217  wepwsolem  44315  mendring  44451  mendlmod  44452  hausgraph  44468  cantnftermord  44583  cantnfub  44584  cantnf2  44588  omabs2  44595  rp-isfinite5  44779  omelaxinf2  46243  cncmpmax  46323  eliinid  46399  icccncfext  47170  dvnprodlem2  47230  stoweidlem7  47290  stoweidlem34  47317  stoweidlem35  47318  stoweidlem59  47342  stoweidlem60  47343  stoweidlem62  47345  fourierdlem34  47424  fourierdlem73  47462  fourierdlem77  47466  etransclem35  47552  smfsuplem2  48095  pgrple2abl  49808  clddisj  50349  sinhadd  51254  veroquadgsumlem  51411