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  6209  ordin  6416  fimacnvdisj  6787  f1oexrnex  7950  wemoiso  7997  wemoiso2  7998  smocdmdom  8407  rdglim  8465  oaabs  8685  ecref  8789  ssctOLD  9091  f1oenfi  9217  f1oenfirn  9218  f1domfi  9219  domfi  9227  sdomdomtrfi  9239  php  9245  onomeneqOLD  9264  f1vrnfibi  9380  brwdom2  9611  infdiffi  9696  cantnflem1  9727  wemapwe  9735  cnfcom3lem  9741  r1lim  9810  carduni  10019  ac5num  10074  infunsdom1  10250  cofsmo  10307  isf32lem6  10396  hsmexlem1  10464  ac6c4  10519  fnct  10575  pwfseqlem1  10696  tskuni  10821  recgt1i  12163  avgle2  12505  eluzmn  12883  rpnnen1lem1  13018  xnn0le2is012  13285  fzneuz  13645  mulmod0  13914  hasheni  14384  hashun2  14419  hashf1dmrn  14479  reccn2  15630  isershft  15697  sumeq2ii  15726  prodeq2ii  15944  demoivreALT  16234  bitsp1  16465  gcdneg  16556  eucalginv  16618  eucalg  16621  odzdvds  16829  fldivp1  16931  prmunb  16948  vdwap1  17011  setsid  17242  acsmapd  18612  intopsn  18680  cntzidss  19371  symggrp  19433  pmtrfv  19485  odmodnn0  19573  sylow2alem1  19650  telgsumfzs  20022  dprdsn  20071  dvdsrmul1  20386  dvrid  20423  cntzsubrng  20584  znunit  21600  isphld  21690  frlmup1  21836  evl1val  22349  evl1sca  22354  pf1const  22366  mat1f1o  22500  mat1mhm  22506  matunit  22700  pm2mpmhmlem2  22841  cctop  23029  iscnp4  23287  iscncl  23293  cnntr  23299  tx2cn  23634  xkoco1cn  23681  qtopkgen  23734  hmeontr  23793  hmeores  23795  filssufilg  23935  ustuqtop1  24266  utop2nei  24275  fmucndlem  24316  cfilufg  24318  xmetres2  24387  metres2  24389  metustto  24582  metust  24587  cfilucfil  24588  dscopn  24602  nmoi  24765  iccntr  24857  cphsqrtcl2  25234  cmsss  25399  ivthlem3  25502  sca2rab  25561  ovolicc2lem3  25568  mdegleb  26118  mdegmullem  26132  aalioulem3  26391  ulm2  26443  ulmcn  26457  root1eq1  26813  atanlogsublem  26973  birthdaylem3  27011  logexprlim  27284  dchrisumlem3  27550  f1otrg  28894  ax5seglem1  28958  ax5seglem2  28959  ax5seglem3a  28960  ax5seglem4  28962  ax5seglem9  28967  ax5seg  28968  axbtwnid  28969  axlowdimlem17  28988  axcontlem2  28995  axcontlem4  28997  axcontlem8  29001  rusgrnumwwlks  30004  wwlksext2clwwlk  30086  grpoidinv  30537  imsmetlem  30719  ipasslem1  30860  ip2eqi  30885  hvpncan  31068  pjid  31724  hmopre  31952  eigvalcl  31990  leopnmid  32167  superpos  32383  cvp  32404  rabfodom  32533  xlt2addrd  32769  hashxpe  32817  cyc3genpmlem  33154  lmodslmd  33193  elrgspnlem4  33235  nsgqusf1olem2  33422  elrspunidl  33436  prmidl0  33458  rsprprmprmidlb  33531  irngnminplynz  33720  locfinreflem  33801  zarcls0  33829  fmcncfil  33892  rge0scvg  33910  esumfsup  34051  esumcvg  34067  insiga  34118  ballotlemirc  34513  signstfvcl  34567  signsvfn  34576  upgracycusgr  35140  subfacp1lem6  35170  satfdmlem  35353  msubff1  35541  fv2ndcnv  35759  matunitlindf  37605  ovoliunnfl  37649  voliunnfl  37651  volsupnfl  37652  ftc1anclem5  37684  indexa  37720  sstotbnd3  37763  heiborlem6  37803  rngosn3  37911  atlatmstc  39301  atlatle  39302  glbconN  39359  glbconNOLD  39360  intnatN  39390  lnnat  39410  atcvrj2b  39415  atexchcvrN  39423  llncvrlpln  39541  lplncvrlvol  39599  lautcvr  40075  trlatn0  40155  cdleme48fvg  40483  cdlemg33c  40691  dihcl  41253  imadomfi  41984  fsuppssind  42580  elpell1qr2  42860  oddcomabszz  42933  wepwsolem  43031  mendring  43177  mendlmod  43178  hausgraph  43194  cantnftermord  43310  cantnfub  43311  cantnf2  43315  omabs2  43322  rp-isfinite5  43507  cncmpmax  44970  eliinid  45051  icccncfext  45843  dvnprodlem2  45903  stoweidlem7  45963  stoweidlem34  45990  stoweidlem35  45991  stoweidlem59  46015  stoweidlem60  46016  stoweidlem62  46018  fourierdlem34  46097  fourierdlem73  46135  fourierdlem77  46139  etransclem35  46225  smfsuplem2  46768  pgrple2abl  48210  clddisj  48700