Theorem simpr2 1061

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

Assertion

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

Proof of Theorem simpr2

Step	Hyp	Ref	Expression
1		simp2 1055	. 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:  simplr2  1097  simprr2  1103  simp1r2  1151  simp2r2  1157  simp3r2  1163  3anandis  1426  fpr2g  6380  isopolem  6495  fr3nr  6871  frfi  8090  intrnfi  8205  fisupcl  8258  cnfcomlem  8479  ackbij1lem15  8939  cofsmo  8974  sornom  8982  fpwwe2lem5  9335  dedekindle  10080  supmul1  10869  eluzuzle  11572  xlesubadd  11965  elioc2  12107  elico2  12108  elicc2  12109  fseq1p1m1  12283  fz0fzelfz0  12314  swrdsbslen  13300  swrdspsleq  13301  ccatswrd  13308  swrdswrdlem  13311  tanadd  14736  dvds2ln  14852  cshwsidrepsw  15638  ressress  15765  f1ovscpbl  16009  mreexexlem4d  16130  mreexexd  16131  mreexexdOLD  16132  iscatd2  16165  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  latjass  16918  latj12  16919  latj32  16920  latj13  16921  latj31  16922  latjrot  16923  latjjdi  16926  latjjdir  16927  latdisdlem  17012  prdsmndd  17146  frmdmnd  17219  grpsubrcan  17319  grpsubadd  17326  grpaddsubass  17328  grpsubsub4  17331  grppnpcan2  17332  grpnpncan  17333  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  fvcosymgeq  17672  pmtrprfv  17696  psgnunilem3  17739  cmn32  18034  cmn12  18036  abladdsub  18043  ablsubsub23  18053  mulgdi  18055  mulgsubdi  18058  dprdss  18251  dprdz  18252  dprdf1o  18254  dprdsn  18258  dprd2da  18264  dmdprdsplit  18269  ablfac1b  18292  pgpfac1lem5  18301  srgi  18334  srgbinom  18368  ringi  18383  prdsringd  18435  opprring  18454  mulgass3  18460  dvrass  18513  subrgunit  18621  issubrg2  18623  abvdiv  18660  lsssn0  18769  islss3  18780  prdslmodd  18790  islmhm2  18859  lspsolv  18964  islbs2  18975  islbs3  18976  lbsextlem4  18982  sralmod  19008  issubassa  19145  sraassa  19146  psrbaglesupp  19189  psrbaglecl  19190  psrbagcon  19192  psrgrp  19219  psrlmod  19222  psrring  19232  psrassa  19235  psgndiflemB  19765  ipdir  19803  ipdi  19804  ipsubdir  19806  ipsubdi  19807  ipass  19809  ipassr  19810  ipassr2  19811  isphld  19818  ocvlss  19835  mamudm  20013  matring  20068  matassa  20069  ofco2  20076  ma1repveval  20196  mdetunilem1  20237  mdetunilem9  20245  chpscmatgsumbin  20468  iinopn  20532  restopnb  20789  subbascn  20868  nrmsep2  20970  isnrm3  20973  regsep2  20990  dnsconst  20992  dfcon2  21032  1stcelcls  21074  dislly  21110  ptuni2  21189  tx1stc  21263  0nelfb  21445  infil  21477  fsubbas  21481  filssufilg  21525  hauspwpwf1  21601  cnextcn  21681  tmdcn2  21703  ustuqtoplem  21853  utopsnneiplem  21861  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  icoopnst  22546  pi1grplem  22657  clmpm1dir  22711  cmodscmulexp  22730  cvsdiv  22740  cvsdivcl  22741  cphdivcl  22790  cphsubdir  22816  cphsubdi  22817  tchcph  22844  bcthlem5  22933  volfiniun  23122  volcn  23180  itg1val2  23257  dvconst  23486  dvlip  23560  ftc1a  23604  ulmval  23938  ulmdvlem3  23960  ang180  24344  cvxcl  24511  scvxcvx  24512  sgmmul  24726  dchrabl  24779  gausslemma2dlem1a  24890  motgrp  25238  iscgra1  25502  cgrane1  25504  cgrane3  25506  cgrahl1  25508  cgrahl2  25509  cgracgr  25510  cgratr  25515  cgrabtwn  25517  cgrahl  25518  dfcgra2  25521  sacgr  25522  f1otrge  25552  colinearalglem1  25586  axcgrtr  25595  axeuclidlem  25642  axcontlem3  25646  axcontlem4  25647  axcontlem7  25650  eengtrkg  25665  eengtrkge  25666  isspthonpth  26114  wlkdvspth  26138  clwlkfoclwwlk  26372  el2spthonot0  26398  el2wlkonotot0  26399  usg2wotspth  26411  2spontn0vne  26414  rusgranumwlks  26483  rusgranumwwlkg  26486  iseupa  26492  3vfriswmgra  26532  frgrareggt1  26643  grpomuldivass  26779  ablomuldiv  26790  ablodivdiv4  26792  ablonnncan1  26796  nvmdi  26887  dipassr  27085  archiabllem2c  29080  dvrdir  29121  dvrcan5  29124  reofld  29171  pstmfval  29267  qqhval2lem  29353  qqhvq  29359  measdivcstOLD  29614  measdivcst  29615  carsggect  29707  bnj1098  30108  bnj149  30199  bnj1118  30306  erdszelem9  30435  rescon  30482  cvmseu  30512  cvmlift2lem10  30548  cvmlift2lem12  30550  elmrsubrn  30671  mclsind  30721  frrlem4  31027  cgrid2  31280  segconeu  31288  btwncomim  31290  btwnswapid  31294  trisegint  31305  cgrxfr  31332  brofs2  31354  endofsegid  31362  btwnconn2  31379  seglemin  31390  segletr  31391  btwnsegle  31394  colinbtwnle  31395  broutsideof2  31399  btwnoutside  31402  broutsideof3  31403  outsideoftr  31406  outsidele  31409  fvray  31418  fvline  31421  ellines  31429  broucube  32613  ftc1anc  32663  sdclem1  32709  sstotbnd2  32743  iscringd  32967  lsmsat  33313  lfladdcl  33376  lflnegcl  33380  lflvscl  33382  eqlkr  33404  lshpkrlem4  33418  lshpkrlem6  33420  ldualgrplem  33450  lduallmodlem  33457  latmassOLD  33534  latm12  33535  latm32  33536  latmrot  33537  latmmdiN  33539  latmmdir  33540  omlfh1N  33563  omlfh3N  33564  cvrnbtwn2  33580  cvlexchb1  33635  cvlsupr2  33648  hlatjass  33674  hlatj12  33675  hlatj32  33676  cvrat  33726  cvrat2  33733  atltcvr  33739  atexchltN  33745  cvrat3  33746  cvrat4  33747  atbtwnexOLDN  33751  atbtwnex  33752  3dimlem3  33765  3dimlem3OLDN  33766  3at  33794  2atneat  33819  llncmp  33826  2at0mat0  33829  2atmat0  33830  llncvrlpln  33862  lplncmp  33866  2llnjaN  33870  4atlem11  33913  lplncvrlvol  33920  lvolcmp  33921  2atm2atN  34089  elpaddatriN  34107  paddasslem8  34131  paddass  34142  padd12N  34143  paddssw2  34148  paddss  34149  pmod1i  34152  pmodN  34154  pmapjlln1  34159  atmod1i1  34161  atmod1i2  34163  pexmidlem2N  34275  pl42lem2N  34284  pl42lem3N  34285  pl42lem4N  34286  pl42N  34287  lhpm0atN  34333  lautlt  34395  lautcvr  34396  lautj  34397  lautm  34398  ltrneq2  34452  cdlemd1  34503  cdleme1b  34531  cdleme1  34532  cdleme2  34533  cdleme3e  34537  cdlemefr27cl  34709  cdlemefs27cl  34719  cdleme42ke  34791  cdleme42mN  34793  cdlemf2  34868  cdlemftr2  34872  trljco  35046  tgrpgrplem  35055  tendoplass  35089  tendodi1  35090  tendodi2  35091  cdlemk34  35216  cdlemk36  35219  erngdvlem3-rN  35304  tendospdi1  35327  dialss  35353  dvhvaddass  35404  dvhopvsca  35409  dvhlveclem  35415  diblss  35477  diclss  35500  diclspsn  35501  cdlemn11pre  35517  dihmeetlem12N  35625  dihmeetlem16N  35629  dihmeetlem17N  35630  dihmeetlem18N  35631  dvh4dimN  35754  lpolconN  35794  dochpolN  35797  lclkr  35840  lclkrs  35846  lcfr  35892  irrapxlem6  36409  jm2.26lem3  36586  dgrsub2  36724  mpaaroot  36744  mendring  36781  mendlmod  36782  mendassa  36783  relexpmulg  37021  iunrelexpmin2  37023  relexpxpmin  37028  neicvgel1  37437  rfcnpre3  38215  fmuldfeq  38650  stoweidlem43  38936  stoweidlem52  38945  stoweidlem53  38946  stoweidlem56  38949  stoweidlem57  38950  stoweidlem60  38953  issmfle  39632  issmfgt  39643  issmfge  39656  smflimlem4  39660  iccpartigtl  39961  iccelpart  39971  ltsubsubaddltsub  40347  subgruhgredgd  40508  nbfusgrlevtxm2  40606  upgr1wlkwlk  40847  lfgriswlk  40897  1wlkiswwlksupgr2  41074  umgrwwlks2on  41161  rusgrnumwwlks  41177  3spthd  41343  3vfriswmgr  41448  frgr2wwlkeqm  41496  av-numclwwlk2  41537  av-numclwwlk3  41539  av-numclwwlk5  41542  copissgrp  41598  cznrng  41747  funcringcsetcALTV2lem9  41836  funcringcsetclem9ALTV  41859  ldepsprlem  42055  lincresunit3  42064  lincreslvec3  42065