Theorem simpl2 1058

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

Assertion

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

Proof of Theorem simpl2

Step	Hyp	Ref	Expression
1		simp2 1055	. 2 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜓)
2	1	adantr 480	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:  simpll2  1094  simprl2  1100  simp1l2  1148  simp2l2  1154  simp3l2  1160  3anandirs  1427  rspc3ev  3297  f1prex  6439  weniso  6504  ofmpteq  6814  tfisi  6950  mpt2sn  7155  smogt  7351  smorndom  7352  omeulem1  7549  nnmord  7599  nnmword  7600  difsnen  7927  enfixsn  7954  mapunen  8014  ac6sfi  8089  ordiso2  8303  wemaplem2  8335  wemapso  8339  wemapso2lem  8340  en2eqpr  8713  acndom  8757  infmap2  8923  cflim2  8968  cfsmolem  8975  coftr  8978  fin23lem26  9030  isf32lem9  9066  fin1a2lem9  9113  fin1a2lem10  9114  ac6num  9184  gchdomtri  9330  canth4  9348  gchpwdom  9371  gruima  9503  grudomon  9518  prn0  9690  distrlem4pr  9727  prlem934  9734  addcan  10099  addcan2  10100  divmulass  10587  divmulasscom  10588  ltmul1a  10751  supmul1  10869  uzsupss  11656  xaddass  11951  xleadd1a  11955  xlesubadd  11965  xmulass  11989  xlemul2a  11991  xadddilem  11996  xadddi  11997  ixxdisj  12061  ixxun  12062  ixxlb  12068  icoshftf1o  12166  icodisj  12168  lincmb01cmp  12186  iccf1o  12187  ssfzoulel  12428  modmuladd  12574  modaddmulmod  12599  ltexp2a  12774  leexp2  12777  ltexp2r  12779  exple1  12782  expnlbnd2  12857  mulsubdivbinom2  12908  fun2dmnop0  13131  ccatass  13224  ccatopth  13322  swrdccatin12lem2a  13336  repswccat  13383  cshwidxmodr  13401  2cshw  13410  repsco  13436  s2f1o  13511  limsupgle  14056  limsupgre  14060  addcn2  14172  mulcn2  14174  binomrisefac  14612  dvdsval2  14824  dvdsadd2b  14866  dvdsmod  14888  oexpneg  14907  sadass  15031  gcdass  15102  rplpwr  15114  rppwr  15115  lcmass  15165  coprmdvds2  15206  rpmulgcd2  15208  rpdvds  15212  coprmprod  15213  cncongr2  15220  rpexp  15270  prmdiveq  15329  hashgcdlem  15331  odzdvds  15338  coprimeprodsq2  15352  pythagtriplem3  15361  pythagtriplem4  15362  pcdvdsb  15411  vdwnnlem1  15537  0ram  15562  ramz2  15566  ramub1lem1  15568  mremre  16087  mrieqv2d  16122  lubss  16944  lubun  16946  clatleglb  16949  clatglbss  16950  mrelatglb  17007  isnsgrp  17111  issubmnd  17141  gsumccat  17201  frmdss2  17223  nmzsubg  17458  ghmnsgima  17507  gsmsymgreqlem1  17673  psgnunilem4  17740  odmodnn0  17782  odnncl  17787  odmod  17788  oddvds  17789  odeq  17792  odmulgid  17794  odmulgeq  17797  odbezout  17798  odf1o1  17810  odf1o2  17811  odngen  17815  gexdvdsi  17821  pgpfi1  17833  odcau  17842  subgslw  17854  fislw  17863  lsmless1x  17882  lsmless2x  17883  lsmsubm  17891  lsmmod  17911  lsmmod2  17912  efgsfo  17975  odadd1  18074  odadd2  18075  odadd  18076  lsmcomx  18082  prdscmnd  18087  gsumconst  18157  srg1zr  18352  csrgbinom  18369  ring1eq0  18413  mulgass2  18424  cntzsubr  18635  isabvd  18643  0lmhm  18861  lmhmvsca  18866  reslmhm2b  18875  pwssplit1  18880  pwssplit2  18881  pwssplit3  18882  lbspss  18903  lspsnat  18966  lidldvgen  19076  issubassa  19145  evlsval2  19341  coe1subfv  19457  coe1sclmul  19473  coe1sclmul2  19475  xrsdsreclblem  19611  cssmre  19856  obs2ss  19892  uvcresum  19951  frlmsslsp  19954  frlmup4  19959  lindff1  19978  f1lindf  19980  lsslindf  19988  islindf4  19996  mpt2matmul  20071  mamutpos  20083  scmatscmide  20132  mavmulsolcl  20176  mulmarep1gsum2  20199  mdetdiaglem  20223  mdetdiag  20224  mdetunilem1  20237  mdetunilem3  20239  mdetunilem9  20245  maducoeval2  20265  madurid  20269  slesolinvbi  20306  cramerimplem1  20308  cramerlem1  20312  cramer  20316  cpmatel2  20337  m2cpm  20365  m2pmfzmap  20371  m2cpminvid2lem  20378  m2cpminvid2  20379  decpmatmul  20396  pmatcollpw1lem2  20399  pmatcollpw1  20400  pmatcollpw2lem  20401  pmatcollpwfi  20406  pm2mpcl  20421  mply1topmatcl  20429  mp2pm2mplem2  20431  mp2pm2mplem4  20433  mp2pm2mplem5  20434  mp2pm2mp  20435  pm2mpghmlem2  20436  pm2mpghmlem1  20437  chfacfisfcpmat  20479  topssnei  20738  cnconst2  20897  cnpresti  20902  cnprest2  20904  cnpdis  20907  cnt0  20960  cnt1  20964  cnhaus  20968  sscmp  21018  hauscmp  21020  cnconn  21035  uncon  21042  finlocfin  21133  comppfsc  21145  kgen2ss  21168  ptpjopn  21225  prdstopn  21241  ptrescn  21252  qtopss  21328  kqfvima  21343  fbssint  21452  fbasrn  21498  filuni  21499  fmss  21560  rnelfm  21567  fmufil  21573  fmco  21575  flimss2  21586  flimss1  21587  flimrest  21597  cnpflf2  21614  flfcnp  21618  supnfcls  21634  fclsss1  21636  fclsss2  21637  isfcf  21648  subgntr  21720  opnsubg  21721  cldsubg  21724  ghmcnp  21728  ustuqtop1  21855  bldisj  22013  blgt0  22014  bl2in  22015  blss2ps  22018  blss2  22019  blssps  22039  blss  22040  xmetresbl  22052  lpbl  22118  blcld  22120  stdbdmopn  22133  metcnp3  22155  metcnp  22156  metcnp2  22157  txmetcnp  22162  blval2  22177  nmoix  22343  nmoi2  22344  nmotri  22353  metdsge  22460  metdseq0  22465  iocopnst  22547  xrhmeo  22553  nmhmcn  22728  cphsqrtcl2  22794  cphsqrtcl3  22795  pjth  23018  ovoliunlem2  23078  volun  23120  mbfimaopn2  23230  iblconst  23390  limcvallem  23441  dvfval  23467  dvcnp2  23489  dvcn  23490  deg1mul3le  23680  deg1tmle  23681  dvdsq1p  23724  ig1peu  23735  ig1pdvds  23740  ply1term  23764  coeid3  23800  dgrmulc  23831  dvply1  23843  aaliou2  23899  efcvx  24007  tanord  24088  eflogeq  24152  logdivlti  24170  logccv  24209  recxpcl  24221  cxplea  24242  cxpeq  24298  ang180  24344  isosctrlem2  24349  cxp2lim  24503  amgm  24517  muval1  24659  dvdssqf  24664  mumullem2  24706  mumul  24707  bcmono  24802  lgsneg  24846  lgsdilem  24849  lgsdirprm  24856  lgsdir  24857  lgsdi  24859  lgsne0  24860  brbtwn2  25585  colinearalglem1  25586  colinearalg  25590  axcgrtr  25595  axsegconlem8  25604  axsegconlem9  25605  axsegconlem10  25606  axcontlem2  25645  axcontlem10  25653  cyclispthon  26161  wwlknext  26252  clwlkisclwwlklem0  26316  erclwwlksym  26342  eleclclwwlknlem2  26346  erclwwlkneqlen  26352  erclwwlknsym  26354  vdgrfval  26422  nbhashuvtx1  26442  usgreghash2spot  26596  extwwlkfablem2  26605  numclwwlk3lem  26635  frgraregord13  26646  nvmul0or  26889  ipval2lem2  26943  lnoadd  26997  lnosub  26998  lnomul  26999  shless  27602  shlej1  27603  kbmul  28198  homco2  28220  kbass2  28360  eliccelico  28929  elicoelioo  28930  iocinioc2  28931  iocinif  28933  difioo  28934  xrge0adddir  29023  xrge0npcan  29025  isarchi2  29070  archiabl  29083  rhmdvdsr  29149  pstmfval  29267  fmcncfil  29305  zrhnm  29341  qqhnm  29362  nexple  29399  volfiniune  29620  dya2iocnrect  29670  probinc  29810  cndprob01  29824  signswmnd  29960  bnj517  30209  cvmsss2  30510  cvmlift2lem10  30548  br6  30900  funsseq  30912  frrlem4  31027  cgrtriv  31279  5segofs  31283  btwnouttr2  31299  btwnxfr  31333  lineext  31353  btwnconn1lem13  31376  brsegle2  31386  nn0prpwlem  31487  lindsenlbs  32574  blbnd  32756  ismtyima  32772  rrndstprj2  32800  ghomdiv  32861  grpokerinj  32862  lsatfixedN  33314  lssat  33321  lshpkrlem4  33418  cvrcon3b  33582  atlen0  33615  atcvreq0  33619  atnle  33622  atlatmstc  33624  atlatle  33625  cvlcvr1  33644  hlsupr2  33691  hlrelat2  33707  cvrexchlem  33723  lnnat  33731  atcvrj2b  33736  3dimlem3  33765  3dim1  33771  1cvrjat  33779  llni  33812  llni2  33816  llnexatN  33825  2llnmat  33828  lplni  33836  2atnelpln  33848  llncvrlpln2  33861  2llnmj  33864  lplnexatN  33867  lplnexllnN  33868  2llnm3N  33873  lvoli  33879  lvoli3  33881  lvolnle3at  33886  islvol2aN  33896  4atlem4a  33903  4atlem4b  33904  4atlem11  33913  lplncvrlvol2  33919  2lplnmj  33926  islinei  34044  linepmap  34079  lnjatN  34084  lncvrat  34086  lncmp  34087  elpaddn0  34104  elpaddatriN  34107  elpaddat  34108  paddcom  34117  paddss2  34122  paddss12  34123  paddasslem4  34127  paddasslem9  34132  paddasslem10  34133  pmodl42N  34155  pmapjoin  34156  llnmod1i2  34164  polcon2bN  34224  pclfinclN  34254  poml4N  34257  poml6N  34259  osumcllem1N  34260  osumcllem2N  34261  osumcllem11N  34270  osumclN  34271  pmapojoinN  34272  pexmidlem2N  34275  pexmidlem3N  34276  pexmidlem4N  34277  pexmidlem6N  34279  pexmidlem7N  34280  pl42lem2N  34284  pl42lem3N  34285  pl42lem4N  34286  pl42N  34287  lhprelat3N  34344  4atex  34380  lauteq  34399  lautco  34401  ltrncoidN  34432  ltrneq2  34452  ltrnideq  34480  trlnle  34491  trlval3  34492  cdlemc  34502  cdlemd9  34511  cdlemd  34512  cdleme21j  34642  cdleme21  34643  cdleme29ex  34680  cdlemefr27cl  34709  cdlemefs27cl  34719  cdleme32d  34750  cdleme32f  34752  cdleme35h2  34763  cdleme40m  34773  cdleme17d3  34802  cdleme48fvg  34806  cdlemeg46fvcl  34812  cdlemeg46fgN  34840  cdleme48fgv  34844  cdleme50trn3  34859  cdlemb3  34912  cdlemg8  34937  cdlemg11a  34943  cdlemg15a  34961  cdlemg15  34962  cdlemg16  34963  cdlemg16z  34965  cdlemg17dN  34969  cdlemg24  34994  cdlemg37  34995  cdlemg29  35011  cdlemg33b  35013  cdlemg38  35021  cdlemg40  35023  trlco  35033  cdlemg44b  35038  ltrncom  35044  trljco  35046  tendococl  35078  tendoplcl  35087  tendoplcom  35088  cdlemj2  35128  tendoid0  35131  tendo1ne0  35134  cdlemk25-3  35210  cdlemk36  35219  cdlemkid4  35240  cdlemk19x  35249  cdlemk53  35263  cdlemk56  35277  cdleml5N  35286  tendospcanN  35330  cdlemm10N  35425  dihord6apre  35563  dihord  35571  dihmeetlem1N  35597  dihglblem2N  35601  dihmeetlem2N  35606  dihmeetbN  35610  dihmeetlem5  35615  dihmeetlem6  35616  dihmeetlem7N  35617  dihmeetlem10N  35623  dihmeetlem12N  35625  dihmeetlem16N  35629  dihmeetlem17N  35630  dihmeetlem18N  35631  dihmeetALTN  35634  dihlspsnssN  35639  dvh3dim2  35755  dvh3dim3N  35756  lcfrlem16  35865  mapdrvallem2  35952  mapdh8ad  36086  hgmapvvlem3  36235  diophrw  36340  eldioph2lem1  36341  diophrex  36357  rencldnfi  36403  pellexlem2  36412  pellqrexplicit  36459  infmrgelbi  36460  pellfundglb  36467  pellfund14gap  36469  rmxycomplete  36500  congadd  36551  acongeq  36568  jm2.19  36578  jm2.23  36581  jm2.20nn  36582  jm2.27  36593  jm3.1  36605  lnmepi  36673  lmhmlnmsplit  36675  hbtlem2  36713  dgraa0p  36738  idomrootle  36792  proot1hash  36797  iocunico  36815  iocinico  36816  relexpxpmin  37028  ntrclsk3  37388  rfcnnnub  38218  uzwo4  38246  supxrge  38495  infleinflem2  38528  snunioo2  38578  iccintsng  38596  climsuse  38675  lptre2pt  38707  limcleqr  38711  0ellimcdiv  38716  fnlimfvre  38741  dvnprodlem1  38836  volioc  38864  stoweidlem17  38910  stoweidlem19  38912  stoweidlem20  38913  stoweidlem22  38915  stoweidlem28  38921  stoweidlem34  38927  stoweidlem44  38937  stoweidlem60  38953  wallispilem3  38960  fourierdlem42  39042  fourierdlem48  39047  fourierdlem51  39050  fourierdlem54  39053  fourierdlem74  39073  fourierdlem77  39076  fourierdlem87  39086  fourierdlem97  39096  ioorrnopnlem  39200  ovnsubaddlem2  39461  fzopredsuc  39946  lighneallem4  40065  oexpnegALTV  40126  oexpnegnz  40127  tgblthelfgott  40229  tgblthelfgottOLD  40236  repswpfx  40299  eluzge0nn0  40350  fzoopth  40360  ewlkle  40807  edginwlk  40839  usgr2trlncl  40966  crctcsh1wlkn0lem5  41017  wwlknp  41045  1wlkiswwlks1  41064  wwlksnext  41099  wspthsnwspthsnon  41122  clwlkclwwlklem3  41210  erclwwlkssym  41242  erclwwlksnsym  41254  upgriseupth  41375  eucrct2eupth  41413  3cyclfrgrrn  41456  av-frgraregord13  41550  rmsupp0  41943  rmsuppss  41945  lincresunit3lem3  42057  lincresunit3lem2  42063  lindssnlvec  42069  fdivmptf  42133  refdivmptf  42134  elbigolo1  42149