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  6142  ordin  6344  fimacnvdisj  6709  f1oexrnex  7866  wemoiso  7914  wemoiso2  7915  smocdmdom  8297  rdglim  8354  oaabs  8572  ecref  8676  f1oenfi  9099  f1oenfirn  9100  f1domfi  9101  domfi  9109  sdomdomtrfi  9121  php  9127  f1vrnfibi  9237  brwdom2  9470  infdiffi  9559  cantnflem1  9590  wemapwe  9598  cnfcom3lem  9604  r1lim  9676  carduni  9885  ac5num  9938  infunsdom1  10114  cofsmo  10171  isf32lem6  10260  hsmexlem1  10328  ac6c4  10383  fnct  10439  pwfseqlem1  10560  tskuni  10685  recgt1i  12030  avgle2  12373  eluzmn  12749  rpnnen1lem1  12882  xnn0le2is012  13152  fzneuz  13515  mulmod0  13788  hasheni  14262  hashun2  14297  hashf1dmrn  14357  reccn2  15511  isershft  15578  sumeq2ii  15607  prodeq2ii  15825  demoivreALT  16117  bitsp1  16349  gcdneg  16440  eucalginv  16502  eucalg  16505  odzdvds  16714  fldivp1  16816  prmunb  16833  vdwap1  16896  setsid  17125  acsmapd  18468  intopsn  18570  cntzidss  19260  symggrp  19320  pmtrfv  19372  odmodnn0  19460  sylow2alem1  19537  telgsumfzs  19909  dprdsn  19958  dvdsrmul1  20296  dvrid  20333  cntzsubrng  20491  znunit  21509  isphld  21600  frlmup1  21744  evl1val  22264  evl1sca  22269  pf1const  22281  mat1f1o  22413  mat1mhm  22419  matunit  22613  pm2mpmhmlem2  22754  cctop  22941  iscnp4  23198  iscncl  23204  cnntr  23210  tx2cn  23545  xkoco1cn  23592  qtopkgen  23645  hmeontr  23704  hmeores  23706  filssufilg  23846  ustuqtop1  24176  utop2nei  24185  fmucndlem  24225  cfilufg  24227  xmetres2  24296  metres2  24298  metustto  24488  metust  24493  cfilucfil  24494  dscopn  24508  nmoi  24663  iccntr  24757  cphsqrtcl2  25133  cmsss  25298  ivthlem3  25401  sca2rab  25460  ovolicc2lem3  25467  mdegleb  26016  mdegmullem  26030  aalioulem3  26289  ulm2  26341  ulmcn  26355  root1eq1  26712  atanlogsublem  26872  birthdaylem3  26910  logexprlim  27183  dchrisumlem3  27449  f1otrg  28869  ax5seglem1  28927  ax5seglem2  28928  ax5seglem3a  28929  ax5seglem4  28931  ax5seglem9  28936  ax5seg  28937  axbtwnid  28938  axlowdimlem17  28957  axcontlem2  28964  axcontlem4  28966  axcontlem8  28970  cyclnumvtx  29799  rusgrnumwwlks  29976  wwlksext2clwwlk  30058  grpoidinv  30509  imsmetlem  30691  ipasslem1  30832  ip2eqi  30857  hvpncan  31040  pjid  31696  hmopre  31924  eigvalcl  31962  leopnmid  32139  superpos  32355  cvp  32376  rabfodom  32506  xlt2addrd  32767  hashxpe  32815  cyc3genpmlem  33161  lmodslmd  33214  elrgspnlem4  33255  elrgspnsubrunlem2  33258  nsgqusf1olem2  33423  elrspunidl  33437  prmidl0  33459  rsprprmprmidlb  33532  extdgfialglem1  33777  irngnminplynz  33797  constrfiss  33836  locfinreflem  33925  zarcls0  33953  fmcncfil  34016  rge0scvg  34034  esumfsup  34155  esumcvg  34171  insiga  34222  ballotlemirc  34617  signstfvcl  34658  signsvfn  34667  upgracycusgr  35271  subfacp1lem6  35301  satfdmlem  35484  msubff1  35672  fv2ndcnv  35894  matunitlindf  37731  ovoliunnfl  37775  voliunnfl  37777  volsupnfl  37778  ftc1anclem5  37810  indexa  37846  sstotbnd3  37889  heiborlem6  37929  rngosn3  38037  atlatmstc  39491  atlatle  39492  glbconN  39549  intnatN  39579  lnnat  39599  atcvrj2b  39604  atexchcvrN  39612  llncvrlpln  39730  lplncvrlvol  39788  lautcvr  40264  trlatn0  40344  cdleme48fvg  40672  cdlemg33c  40880  dihcl  41442  imadomfi  42168  fsuppssind  42751  elpell1qr2  43029  oddcomabszz  43101  wepwsolem  43199  mendring  43345  mendlmod  43346  hausgraph  43362  cantnftermord  43477  cantnfub  43478  cantnf2  43482  omabs2  43489  rp-isfinite5  43674  omelaxinf2  45146  cncmpmax  45193  eliinid  45271  icccncfext  46047  dvnprodlem2  46107  stoweidlem7  46167  stoweidlem34  46194  stoweidlem35  46195  stoweidlem59  46219  stoweidlem60  46220  stoweidlem62  46222  fourierdlem34  46301  fourierdlem73  46339  fourierdlem77  46343  etransclem35  46429  smfsuplem2  46972  pgrple2abl  48527  clddisj  49065