Theorem sylancom 591

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

Syntax hints:   → wi 4   ∧ wa 399

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 400

This theorem is referenced by:  sofld  6030  ordin  6221  fimacnvdisj  6575  f1oexrnex  7683  wemoiso  7724  wemoiso2  7725  smorndom  8083  rdglim  8140  oaabs  8351  ssct  8704  f1oenfi  8836  f1oenfirn  8837  onomeneq  8845  domfi  8874  f1vrnfibi  8939  brwdom2  9167  infdiffi  9251  cantnflem1  9282  wemapwe  9290  cnfcom3lem  9296  r1lim  9353  carduni  9562  ac5num  9615  infunsdom1  9792  cofsmo  9848  isf32lem6  9937  hsmexlem1  10005  ac6c4  10060  fnct  10116  pwfseqlem1  10237  tskuni  10362  recgt1i  11694  avgle2  12036  eluzmn  12410  rpnnen1lem1  12539  xnn0le2is012  12801  fzneuz  13158  mulmod0  13415  hasheni  13879  hashun2  13915  reccn2  15123  isershft  15192  sumeq2ii  15222  prodeq2ii  15438  demoivreALT  15725  bitsp1  15953  gcdneg  16044  eucalginv  16104  eucalg  16107  odzdvds  16311  fldivp1  16413  prmunb  16430  vdwap1  16493  setsid  16719  acsmapd  18014  intopsn  18080  cntzidss  18686  symggrp  18746  pmtrfv  18798  odmodnn0  18886  sylow2alem1  18960  telgsumfzs  19328  dprdsn  19377  dvdsrmul1  19625  dvrid  19660  znunit  20482  isphld  20570  frlmup1  20714  evl1val  21199  evl1sca  21204  pf1const  21216  mat1f1o  21329  mat1mhm  21335  matunit  21529  pm2mpmhmlem2  21670  cctop  21857  iscnp4  22114  iscncl  22120  cnntr  22126  tx2cn  22461  xkoco1cn  22508  qtopkgen  22561  hmeontr  22620  hmeores  22622  filssufilg  22762  ustuqtop1  23093  utop2nei  23102  fmucndlem  23142  cfilufg  23144  xmetres2  23213  metres2  23215  metustto  23405  metust  23410  cfilucfil  23411  dscopn  23425  nmoi  23580  iccntr  23672  cphsqrtcl2  24037  cmsss  24202  ivthlem3  24304  sca2rab  24363  ovolicc2lem3  24370  mdegleb  24916  mdegmullem  24930  aalioulem3  25181  ulm2  25231  ulmcn  25245  root1eq1  25595  atanlogsublem  25752  birthdaylem3  25790  logexprlim  26060  dchrisumlem3  26326  f1otrg  26916  ax5seglem1  26973  ax5seglem2  26974  ax5seglem3a  26975  ax5seglem4  26977  ax5seglem9  26982  ax5seg  26983  axbtwnid  26984  axlowdimlem17  27003  axcontlem2  27010  axcontlem4  27012  axcontlem8  27016  rusgrnumwwlks  28012  wwlksext2clwwlk  28094  grpoidinv  28543  imsmetlem  28725  ipasslem1  28866  ip2eqi  28891  hvpncan  29074  pjid  29730  hmopre  29958  eigvalcl  29996  leopnmid  30173  superpos  30389  cvp  30410  rabfodom  30524  xlt2addrd  30755  hashxpe  30801  cyc3genpmlem  31091  lmodslmd  31130  nsgqusf1olem2  31267  elrspunidl  31274  prmidl0  31294  locfinreflem  31458  zarcls0  31486  fmcncfil  31549  rge0scvg  31567  esumfsup  31704  esumcvg  31720  insiga  31771  ballotlemirc  32164  signstfvcl  32218  signsvfn  32227  hashf1dmrn  32742  upgracycusgr  32784  subfacp1lem6  32814  satfdmlem  32997  msubff1  33185  fv2ndcnv  33422  matunitlindf  35461  ovoliunnfl  35505  voliunnfl  35507  volsupnfl  35508  ftc1anclem5  35540  indexa  35577  sstotbnd3  35620  heiborlem6  35660  rngosn3  35768  atlatmstc  37019  atlatle  37020  glbconN  37077  intnatN  37107  lnnat  37127  atcvrj2b  37132  atexchcvrN  37140  llncvrlpln  37258  lplncvrlvol  37316  lautcvr  37792  trlatn0  37872  cdleme48fvg  38200  cdlemg33c  38408  dihcl  38970  fsuppssind  39933  elpell1qr2  40338  oddcomabszz  40410  wepwsolem  40511  mendring  40661  mendlmod  40662  hausgraph  40681  rp-isfinite5  40750  cncmpmax  42189  eliinid  42275  icccncfext  43046  dvnprodlem2  43106  stoweidlem7  43166  stoweidlem34  43193  stoweidlem35  43194  stoweidlem59  43218  stoweidlem60  43219  stoweidlem62  43221  fourierdlem34  43300  fourierdlem73  43338  fourierdlem77  43342  etransclem35  43428  smfsuplem2  43960  pgrple2abl  45317  clddisj  45813