Theorem sylancom 587

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 583	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  6218  ordin  6425  fimacnvdisj  6799  f1oexrnex  7967  wemoiso  8014  wemoiso2  8015  smocdmdom  8424  rdglim  8482  oaabs  8704  ecref  8808  ssctOLD  9118  f1oenfi  9245  f1oenfirn  9246  f1domfi  9247  domfi  9255  sdomdomtrfi  9267  php  9273  onomeneqOLD  9292  f1vrnfibi  9410  brwdom2  9642  infdiffi  9727  cantnflem1  9758  wemapwe  9766  cnfcom3lem  9772  r1lim  9841  carduni  10050  ac5num  10105  infunsdom1  10281  cofsmo  10338  isf32lem6  10427  hsmexlem1  10495  ac6c4  10550  fnct  10606  pwfseqlem1  10727  tskuni  10852  recgt1i  12192  avgle2  12534  eluzmn  12910  rpnnen1lem1  13043  xnn0le2is012  13308  fzneuz  13665  mulmod0  13928  hasheni  14397  hashun2  14432  hashf1dmrn  14492  reccn2  15643  isershft  15712  sumeq2ii  15741  prodeq2ii  15959  demoivreALT  16249  bitsp1  16477  gcdneg  16568  eucalginv  16631  eucalg  16634  odzdvds  16842  fldivp1  16944  prmunb  16961  vdwap1  17024  setsid  17255  acsmapd  18624  intopsn  18692  cntzidss  19380  symggrp  19442  pmtrfv  19494  odmodnn0  19582  sylow2alem1  19659  telgsumfzs  20031  dprdsn  20080  dvdsrmul1  20395  dvrid  20432  cntzsubrng  20593  znunit  21605  isphld  21695  frlmup1  21841  evl1val  22354  evl1sca  22359  pf1const  22371  mat1f1o  22505  mat1mhm  22511  matunit  22705  pm2mpmhmlem2  22846  cctop  23034  iscnp4  23292  iscncl  23298  cnntr  23304  tx2cn  23639  xkoco1cn  23686  qtopkgen  23739  hmeontr  23798  hmeores  23800  filssufilg  23940  ustuqtop1  24271  utop2nei  24280  fmucndlem  24321  cfilufg  24323  xmetres2  24392  metres2  24394  metustto  24587  metust  24592  cfilucfil  24593  dscopn  24607  nmoi  24770  iccntr  24862  cphsqrtcl2  25239  cmsss  25404  ivthlem3  25507  sca2rab  25566  ovolicc2lem3  25573  mdegleb  26123  mdegmullem  26137  aalioulem3  26394  ulm2  26446  ulmcn  26460  root1eq1  26816  atanlogsublem  26976  birthdaylem3  27014  logexprlim  27287  dchrisumlem3  27553  f1otrg  28897  ax5seglem1  28961  ax5seglem2  28962  ax5seglem3a  28963  ax5seglem4  28965  ax5seglem9  28970  ax5seg  28971  axbtwnid  28972  axlowdimlem17  28991  axcontlem2  28998  axcontlem4  29000  axcontlem8  29004  rusgrnumwwlks  30007  wwlksext2clwwlk  30089  grpoidinv  30540  imsmetlem  30722  ipasslem1  30863  ip2eqi  30888  hvpncan  31071  pjid  31727  hmopre  31955  eigvalcl  31993  leopnmid  32170  superpos  32386  cvp  32407  rabfodom  32533  xlt2addrd  32765  hashxpe  32814  cyc3genpmlem  33144  lmodslmd  33183  nsgqusf1olem2  33407  elrspunidl  33421  prmidl0  33443  rsprprmprmidlb  33516  irngnminplynz  33705  locfinreflem  33786  zarcls0  33814  fmcncfil  33877  rge0scvg  33895  esumfsup  34034  esumcvg  34050  insiga  34101  ballotlemirc  34496  signstfvcl  34550  signsvfn  34559  upgracycusgr  35123  subfacp1lem6  35153  satfdmlem  35336  msubff1  35524  fv2ndcnv  35741  matunitlindf  37578  ovoliunnfl  37622  voliunnfl  37624  volsupnfl  37625  ftc1anclem5  37657  indexa  37693  sstotbnd3  37736  heiborlem6  37776  rngosn3  37884  atlatmstc  39275  atlatle  39276  glbconN  39333  glbconNOLD  39334  intnatN  39364  lnnat  39384  atcvrj2b  39389  atexchcvrN  39397  llncvrlpln  39515  lplncvrlvol  39573  lautcvr  40049  trlatn0  40129  cdleme48fvg  40457  cdlemg33c  40665  dihcl  41227  imadomfi  41959  fsuppssind  42548  elpell1qr2  42828  oddcomabszz  42901  wepwsolem  42999  mendring  43149  mendlmod  43150  hausgraph  43166  cantnftermord  43282  cantnfub  43283  cantnf2  43287  omabs2  43294  rp-isfinite5  43479  cncmpmax  44932  eliinid  45013  icccncfext  45808  dvnprodlem2  45868  stoweidlem7  45928  stoweidlem34  45955  stoweidlem35  45956  stoweidlem59  45980  stoweidlem60  45981  stoweidlem62  45983  fourierdlem34  46062  fourierdlem73  46100  fourierdlem77  46104  etransclem35  46190  smfsuplem2  46733  pgrple2abl  48090  clddisj  48583