Theorem simp1r 1200

Description: Simplification of triple conjunction. (Contributed by NM, 9-Nov-2011.)

Assertion

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

Proof of Theorem simp1r

Step	Hyp	Ref	Expression
1		simpr 484	. 2 ⊢ ((𝜑 ∧ 𝜓) → 𝜓)
2	1	3ad2ant1 1134	1 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒 ∧ 𝜃) → 𝜓)

Syntax hints:   → wi 4   ∧ wa 395   ∧ w3a 1087

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  df-3an 1089

This theorem is referenced by:  simp11r  1287  simp21r  1293  simp31r  1299  eqfunresadj  7315  offsplitfpar  8069  poseq  8108  omeulem2  8518  uniinqs  8744  unxpdomlem3  9168  elfiun  9343  cofsmo  10191  isfin2-2  10241  isf32lem9  10283  tskun  10709  tskurn  10712  reclem3pr  10972  dedekind  11309  subaddmulsub  11613  dmdcan  11865  lt2msq1  12040  supmullem1  12126  supmul  12128  xaddass2  13202  xlt2add  13212  xmulasslem3  13238  iccsplit  13438  expaddzlem  14067  expaddz  14068  expmulz  14070  limsupgle  15439  o1add  15576  o1mul  15577  o1sub  15578  bitsfzo  16404  sadfval  16421  smufval  16446  nn0rppwr  16530  prmexpb  16689  4sqlem18  16933  vdwlem10  16961  setsstruct2  17144  mrieqv2d  17605  curf1  18191  chnccat  18592  mgmsscl  18613  mndpfsupp  18735  mndodcong  19517  subgabl  19811  gex2abl  19826  ogrpinvlt  20119  cntzsubrng  20544  cntzsubr  20583  abvres  20808  lbsind2  21076  lbsextlem2  21157  lbsextg  21160  matring  22408  mdetunilem8  22584  maducoeval  22604  maducoeval2  22605  madurid  22609  cramerimplem3  22650  pmatcollpw2  22743  pm2mpf1  22764  cnprest  23254  isreg2  23342  fbssfi  23802  hausflimlem  23944  tmdgsum  24060  ssblps  24387  ssbl  24388  xrsmopn  24778  cphassi  25181  cphassir  25182  4cphipval2  25209  cphipval  25210  dvres2  25879  vieta1  26278  aalioulem4  26301  efgh  26505  cxpadd  26643  cxpsub  26646  divcxp  26651  cxple2  26661  cxplt2  26662  cxpcn3lem  26711  angcan  26766  ang180lem5  26777  isosctrlem3  26784  lgssq  27300  nosupinfsep  27696  noetalem1  27705  noeta2  27753  ltslpss  27900  bdayfinbndlem1  28459  brbtwn2  28974  axcontlem4  29036  axcontlem8  29040  uhgr2edg  29277  chscllem4  31711  cshwrnid  33021  pstmval  34039  measinblem  34364  cvmlift2lem6  35490  linethru  36335  cnres2  38084  lcv1  39487  lfl1  39516  lshpkrex  39564  hlrelat3  39858  cvrval3  39859  cvrval4N  39860  athgt  39902  atcvrlln2  39965  atcvrlln  39966  lvolnle3at  40028  lvolnlelpln  40031  4atlem11  40055  4atlem12  40058  2lplnj  40066  dalemddea  40130  cdlema2N  40238  paddasslem2  40267  atmod1i1m  40304  lhp2lt  40447  lhp0lt  40449  lhpexle3lem  40457  lhpj1  40468  lhpmcvr4N  40472  lhpelim  40483  lhpmod2i2  40484  lhpmod6i1  40485  cdlemb2  40487  lhpat  40489  ltrnatb  40583  ltrnel  40585  ltrncnvel  40588  ltrncnv  40592  trlval2  40609  trljat1  40612  trljat2  40613  trlnidatb  40623  cdlemc1  40637  cdlemc2  40638  cdlemc5  40641  cdlemc6  40642  cdleme0aa  40656  cdleme0b  40658  cdleme0c  40659  cdleme0e  40663  cdleme0fN  40664  cdleme01N  40667  cdleme0ex1N  40669  cdleme0moN  40671  cdleme3g  40680  cdleme3h  40681  cdleme3  40683  cdleme4  40684  cdleme4a  40685  cdleme5  40686  cdleme8  40696  cdleme9  40699  cdleme10  40700  cdleme16aN  40705  cdleme11fN  40710  cdleme11g  40711  cdleme11k  40714  cdleme13  40718  cdleme17c  40734  cdleme17d1  40735  cdleme18c  40739  cdleme22gb  40740  cdlemeda  40744  cdlemednpq  40745  cdlemednuN  40746  cdleme19c  40751  cdleme20aN  40755  cdleme20bN  40756  cdleme20c  40757  cdleme22aa  40785  cdleme22d  40789  cdleme22e  40790  cdleme27cl  40812  cdleme27a  40813  cdleme30a  40824  cdleme42a  40917  cdleme42c  40918  cdlemg2fv2  41046  cdlemg2m  41050  cdlemg4g  41062  cdlemg4  41063  cdlemg6c  41066  cdlemg7aN  41071  cdlemg9a  41078  cdlemg9b  41079  cdlemg10c  41085  cdlemg12a  41089  cdlemg12b  41090  cdlemg17a  41107  cdlemg18b  41125  cdlemg18c  41126  trlcoabs2N  41168  trlcolem  41172  tendoco2  41214  tendoicl  41242  cdlemi1  41264  cdlemi2  41265  cdlemj3  41269  tendocan  41270  cdlemk3  41279  cdlemk4  41280  cdlemk5a  41281  cdlemk9  41285  cdlemk9bN  41286  cdlemk10  41289  cdlemk30  41340  cdlemk31  41342  cdlemk39  41362  cdlemkfid1N  41367  cdlemkfid2N  41369  cdlemk19ylem  41376  cdlemk19xlem  41388  cdlemk53b  41402  cdlemk53  41403  cdlemk55a  41405  cdlemk43N  41409  cdlemk19u1  41415  cdlemm10N  41564  cdlemn2  41641  cdlemn10  41652  dihjustlem  41662  dihord2cN  41667  dihvalcq2  41693  dihopelvalcpre  41694  dihord5b  41705  dihord6b  41706  dihmeetlem2N  41745  dihmeetbclemN  41750  dihmeetlem4preN  41752  dihmeetALTN  41773  dochshpncl  41830  dochsatshpb  41898  hdmapval3N  42284  hgmap11  42348  f1o2d2  42674  remulcand  42871  pellfundex  43314  congtr  43393  fzmaxdif  43409  isnumbasgrplem2  43532  idomsubgmo  43621  ntrclsk13  44498  grumnudlem  44712  restuni3  45548  unirnmapsn  45643  ssmapsn  45645  infnsuprnmpt  45679  upbdrech  45738  suplesup  45769  infleinf  45801  supxrunb3  45828  mullimc  46046  islptre  46049  mullimcf  46053  neglimc  46075  limsupmnfuzlem  46154  limsupre3lem  46160  limsupre3uzlem  46163  icccncfext  46315  dvmptfprod  46373  stoweidlem31  46459  opnvonmbllem2  47061  smflimsuplem7  47254  ormkglobd  47305  funressneu  47495  cfsetsnfsetf1  47507  prmdvdsfmtnof1lem1  48047  uhgrimisgrgriclem  48406  clnbgrgrim  48410  grlimedgclnbgr  48471  domnmsuppn0  48845  lincext3  48932  2arymaptfo  49130