Theorem simpr1 1060

Description: Simplification rule. (Contributed by Jeff Hankins, 17-Nov-2009.)

Assertion

Ref	Expression
simpr1	⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒 ∧ 𝜃)) → 𝜓)

Proof of Theorem simpr1

Step	Hyp	Ref	Expression
1		simp1 1054	. 2 ⊢ ((𝜓 ∧ 𝜒 ∧ 𝜃) → 𝜓)
2	1	adantl 481	1 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒 ∧ 𝜃)) → 𝜓)

Syntax hints:   → wi 4   ∧ wa 383   ∧ w3a 1031

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 196  df-an 385  df-3an 1033

This theorem is referenced by:  simplr1  1096  simprr1  1102  simp1r1  1150  simp2r1  1156  simp3r1  1162  3anandis  1426  fpr2g  6380  isopolem  6495  fr3nr  6871  suppfnss  7207  frfi  8090  intrnfi  8205  iinfi  8206  eqsup  8245  fisupcl  8258  cnfcomlem  8479  ackbij1lem15  8939  fpwwe2lem5  9335  dedekindle  10080  ico0  12092  elioc2  12107  elico2  12108  elicc2  12109  iccsplit  12176  fseq1p1m1  12283  elfz0ubfz0  12312  hashtpg  13121  swrdsbslen  13300  swrdspsleq  13301  ccatswrd  13308  tanadd  14736  dvds2ln  14852  qredeq  15209  ressress  15765  mreexexlem4d  16130  mreexexd  16131  mreexexdOLD  16132  0catg  16171  2oppccomf  16208  issubc3  16332  fthmon  16410  fuccocl  16447  fucidcl  16448  invfuc  16457  initoeu2lem0  16486  initoeu2lem1  16487  curf2cl  16694  yonedalem4c  16740  yonedalem3  16743  pospo  16796  latjle12  16885  latjlej1  16888  latnlej2  16894  latlem12  16901  latmlem1  16904  latledi  16912  latmlej11  16913  latjass  16918  latj12  16919  latj32  16920  latj13  16921  latj31  16922  latjrot  16923  latjjdi  16926  latjjdir  16927  latdisdlem  17012  prdsmndd  17146  imasmnd2  17150  frmdmnd  17219  grpsubrcan  17319  grpsubadd  17326  grpsubsub  17327  grpaddsubass  17328  grpsubsub4  17331  grpnnncan2  17335  imasgrp2  17353  mulgnndir  17392  mulgnndirOLD  17393  mulgnn0dir  17394  mulgdir  17396  mulgnnass  17399  mulgnnassOLD  17400  mulgnn0ass  17401  mulgass  17402  mulgsubdir  17405  pwsmulg  17410  issubg2  17432  eqgval  17466  qusgrp  17472  galcan  17560  gacan  17561  oppgmnd  17607  symggrp  17643  pmtrprfv  17696  pmtr3ncom  17718  psgnunilem3  17739  cmn32  18034  cmn12  18036  abladdsub  18043  mulgnn0di  18054  mulgdi  18055  mulgsubdi  18058  dprdss  18251  dprdz  18252  dprdf1o  18254  dprdsn  18258  dprd2da  18264  ablfac1b  18292  pgpfac1lem5  18301  srgbinomlem2  18364  srgbinom  18368  ringi  18383  prdsringd  18435  imasring  18442  opprring  18454  mulgass3  18460  dvrass  18513  kerf1hrm  18566  subrgunit  18621  issubrg2  18623  abvdiv  18660  islss3  18780  prdslmodd  18790  islmhm2  18859  lspsolv  18964  islbs2  18975  islbs3  18976  lbsextlem4  18982  sralmod  19008  issubassa  19145  sraassa  19146  psrbaglecl  19190  psrbagcon  19192  psrgrp  19219  psrlmod  19222  psrring  19232  psrassa  19235  ipdir  19803  ipdi  19804  ipsubdir  19806  ipsubdi  19807  ipass  19809  ipassr  19810  ipassr2  19811  ocvlss  19835  mamudm  20013  matring  20068  matassa  20069  ofco2  20076  mdetunilem1  20237  mdetunilem9  20245  mdetuni0  20246  mdetmul  20248  gsummatr01lem3  20282  iinopn  20532  subbascn  20868  nrmsep2  20970  isnrm3  20973  regsep2  20990  dnsconst  20992  dfcon2  21032  1stcelcls  21074  nllyidm  21102  dislly  21110  upxp  21236  fbasne0  21444  filss  21467  infil  21477  fsubbas  21481  filssufilg  21525  tmdcn2  21703  psmettri  21926  isxmet2d  21942  xmettri  21966  xmetres2  21976  bldisj  22013  blss2ps  22018  blss2  22019  xmstri2  22081  mstri2  22082  xmstri  22083  mstri  22084  xmstri3  22085  mstri3  22086  msrtri  22087  comet  22128  stdbdbl  22132  met2ndci  22137  ngprcan  22224  ngplcan  22225  ngpsubcan  22228  nmtri2  22241  nrgdsdi  22279  nrgdsdir  22280  nlmdsdi  22295  nlmdsdir  22296  blcvx  22409  icccmplem2  22434  pi1grplem  22657  pi1cof  22667  clmpm1dir  22711  cvsdiv  22740  cvsdivcl  22741  cphdivcl  22790  cphsubdir  22816  cphsubdi  22817  cphassr  22820  bcthlem5  22933  rrxcph  22988  volfiniun  23122  volcn  23180  itg1val2  23257  dvconst  23486  dvlip  23560  dvfsumlem4  23596  ftc1a  23604  ulmval  23938  ulmdvlem3  23960  ang180  24344  cvxcl  24511  scvxcvx  24512  sgmmul  24726  logexprlim  24750  dchrabl  24779  motgrp  25238  iscgra1  25502  cgrane1  25504  cgrane2  25505  cgrahl1  25508  cgrahl2  25509  cgracgr  25510  cgratr  25515  cgrabtwn  25517  dfcgra2  25521  sacgr  25522  f1otrge  25552  colinearalglem1  25586  colinearalg  25590  axcgrtr  25595  axlowdimlem16  25637  axeuclidlem  25642  axcontlem7  25650  eengtrkg  25665  eengtrkge  25666  wlkoniswlk  26064  constr2trl  26129  wlkdvspth  26138  erclwwlktr  26343  erclwwlkntr  26355  el2spthonot0  26398  el2wlkonotot0  26399  usg2wotspth  26411  2pthwlkonot  26412  iseupa  26492  numclwwlk5  26639  friendship  26649  grpodivdiv  26778  grpomuldivass  26779  ablodivdiv4  26792  ablonnncan  26794  ablonnncan1  26796  nvmdi  26887  dipassr  27085  archiabllem2c  29080  dvrdir  29121  dvrcan5  29124  reofld  29171  pstmfval  29267  tpr2rico  29286  qqhval2lem  29353  qqhvq  29359  issiga  29501  measdivcstOLD  29614  measdivcst  29615  carsggect  29707  signsply0  29954  bnj149  30199  bnj1118  30306  bnj1128  30312  erdszelem9  30435  rescon  30482  cvmseu  30512  cvmlift2lem12  30550  elmrsubrn  30671  mclsind  30721  cgrid2  31280  segconeu  31288  btwncomim  31290  btwnswapid  31294  cgrxfr  31332  btwnxfr  31333  colineardim1  31338  brofs2  31354  brifs2  31355  idinside  31361  endofsegid  31362  btwnconn1lem7  31370  btwnconn1lem11  31374  btwnconn1  31378  segcon2  31382  seglemin  31390  segletr  31391  btwnsegle  31394  colinbtwnle  31395  broutsideof2  31399  broutsideof3  31403  outsidele  31409  fvray  31418  fvline  31421  linerflx1  31426  ellines  31429  ivthALT  31500  poimirlem32  32611  ftc1anc  32663  sdclem1  32709  sstotbnd2  32743  zerdivemp1x  32916  isdrngo2  32927  iscringd  32967  lsmsat  33313  lfladdcl  33376  lflnegcl  33380  lflvscl  33382  lshpkrlem4  33418  lshpkrlem6  33420  ldualgrplem  33450  lduallmodlem  33457  latmassOLD  33534  latm12  33535  latm32  33536  latmrot  33537  latmmdiN  33539  latmmdir  33540  omlfh1N  33563  omlfh3N  33564  cvlexchb1  33635  cvlexch3  33637  cvlexch4N  33638  cvlatexchb1  33639  cvlsupr2  33648  hlatjass  33674  hlatj12  33675  hlatj32  33676  cvratlem  33725  cvrat  33726  atcvrj0  33732  cvrat2  33733  atltcvr  33739  atexchltN  33745  cvrat3  33746  cvrat4  33747  3dimlem3  33765  3dimlem3OLDN  33766  3at  33794  2atneat  33819  llncmp  33826  2at0mat0  33829  2atmat0  33830  lplnnle2at  33845  llncvrlpln  33862  lplncmp  33866  lplnexllnN  33868  2llnjaN  33870  4atlem11  33913  lplncvrlvol  33920  lvolcmp  33921  2atm2atN  34089  elpaddatriN  34107  paddasslem9  34132  paddass  34142  padd12N  34143  paddssw2  34148  paddss  34149  pmodlem2  34151  pmodN  34154  pmapjlln1  34159  atmod1i1  34161  atmod1i2  34163  pexmidlem2N  34275  pexmidlem6N  34279  pl42N  34287  lhpm0atN  34333  lautlt  34395  lautcvr  34396  lautj  34397  lautm  34398  ltrneq2  34452  cdlemc3  34498  cdlemc4  34499  cdlemd1  34503  cdleme1b  34531  cdleme1  34532  cdleme2  34533  cdleme3e  34537  cdlemefr27cl  34709  cdlemefs27cl  34719  cdleme42mN  34793  cdlemftr2  34872  trljco  35046  tgrpgrplem  35055  tendoplass  35089  tendodi1  35090  tendodi2  35091  cdlemk36  35219  erngdvlem3  35296  erngdvlem3-rN  35304  tendospdi1  35327  dvalveclem  35332  dialss  35353  dvhvaddass  35404  dvhopvsca  35409  dvhlveclem  35415  diblss  35477  diclss  35500  dihmeetlem12N  35625  dihmeetlem15N  35628  dihmeetlem16N  35629  dihmeetlem17N  35630  dihmeetlem18N  35631  dihmeetlem19N  35632  dvh4dimN  35754  lpolvN  35793  lclkr  35840  lclkrs  35846  lcfr  35892  irrapxlem6  36409  jm2.26lem3  36586  dgrsub2  36724  mpaadgr  36743  mendring  36781  mendlmod  36782  mendassa  36783  relexpmulg  37021  iunrelexpmin2  37023  relexpxpmin  37028  neicvgel1  37437  fmuldfeq  38650  stoweidlem43  38936  stoweidlem52  38945  stoweidlem53  38946  stoweidlem56  38949  stoweidlem57  38950  issmfle  39632  issmfgt  39643  issmfge  39656  fmtnoprmfac1  40015  fmtnoprmfac2  40017  nbfusgrlevtxm2  40606  upgr1wlkwlk  40847  lfgriswlk  40897  upgrwlkdvde  40943  erclwwlkstr  41243  erclwwlksntr  41255  av-numclwwlk5  41542  av-friendship  41553  copissgrp  41598  cznrng  41747  funcringcsetcALTV2lem9  41836  funcringcsetclem9ALTV  41859  ply1ass23l  41964  linccl  41997  lincext1  42037  lincext3  42039  lincresunit2  42061