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  7308  offsplitfpar  8062  poseq  8101  omeulem2  8511  uniinqs  8737  unxpdomlem3  9161  elfiun  9336  cofsmo  10182  isfin2-2  10232  isf32lem9  10274  tskun  10700  tskurn  10703  reclem3pr  10963  dedekind  11300  subaddmulsub  11604  dmdcan  11856  lt2msq1  12031  supmullem1  12117  supmul  12119  xaddass2  13193  xlt2add  13203  xmulasslem3  13229  iccsplit  13429  expaddzlem  14058  expaddz  14059  expmulz  14061  limsupgle  15430  o1add  15567  o1mul  15568  o1sub  15569  bitsfzo  16395  sadfval  16412  smufval  16437  nn0rppwr  16521  prmexpb  16680  4sqlem18  16924  vdwlem10  16952  setsstruct2  17135  mrieqv2d  17596  curf1  18182  chnccat  18583  mgmsscl  18604  mndpfsupp  18726  mndodcong  19508  subgabl  19802  gex2abl  19817  ogrpinvlt  20110  cntzsubrng  20535  cntzsubr  20574  abvres  20799  lbsind2  21068  lbsextlem2  21149  lbsextg  21152  matring  22418  mdetunilem8  22594  maducoeval  22614  maducoeval2  22615  madurid  22619  cramerimplem3  22660  pmatcollpw2  22753  pm2mpf1  22774  cnprest  23264  isreg2  23352  fbssfi  23812  hausflimlem  23954  tmdgsum  24070  ssblps  24397  ssbl  24398  xrsmopn  24788  cphassi  25191  cphassir  25192  4cphipval2  25219  cphipval  25220  dvres2  25889  vieta1  26289  aalioulem4  26312  efgh  26518  cxpadd  26656  cxpsub  26659  divcxp  26664  cxple2  26674  cxplt2  26675  cxpcn3lem  26724  angcan  26779  ang180lem5  26790  isosctrlem3  26797  lgssq  27314  nosupinfsep  27710  noetalem1  27719  noeta2  27767  ltslpss  27914  bdayfinbndlem1  28473  brbtwn2  28988  axcontlem4  29050  axcontlem8  29054  uhgr2edg  29291  chscllem4  31726  cshwrnid  33036  pstmval  34055  measinblem  34380  cvmlift2lem6  35506  linethru  36351  cnres2  38098  lcv1  39501  lfl1  39530  lshpkrex  39578  hlrelat3  39872  cvrval3  39873  cvrval4N  39874  athgt  39916  atcvrlln2  39979  atcvrlln  39980  lvolnle3at  40042  lvolnlelpln  40045  4atlem11  40069  4atlem12  40072  2lplnj  40080  dalemddea  40144  cdlema2N  40252  paddasslem2  40281  atmod1i1m  40318  lhp2lt  40461  lhp0lt  40463  lhpexle3lem  40471  lhpj1  40482  lhpmcvr4N  40486  lhpelim  40497  lhpmod2i2  40498  lhpmod6i1  40499  cdlemb2  40501  lhpat  40503  ltrnatb  40597  ltrnel  40599  ltrncnvel  40602  ltrncnv  40606  trlval2  40623  trljat1  40626  trljat2  40627  trlnidatb  40637  cdlemc1  40651  cdlemc2  40652  cdlemc5  40655  cdlemc6  40656  cdleme0aa  40670  cdleme0b  40672  cdleme0c  40673  cdleme0e  40677  cdleme0fN  40678  cdleme01N  40681  cdleme0ex1N  40683  cdleme0moN  40685  cdleme3g  40694  cdleme3h  40695  cdleme3  40697  cdleme4  40698  cdleme4a  40699  cdleme5  40700  cdleme8  40710  cdleme9  40713  cdleme10  40714  cdleme16aN  40719  cdleme11fN  40724  cdleme11g  40725  cdleme11k  40728  cdleme13  40732  cdleme17c  40748  cdleme17d1  40749  cdleme18c  40753  cdleme22gb  40754  cdlemeda  40758  cdlemednpq  40759  cdlemednuN  40760  cdleme19c  40765  cdleme20aN  40769  cdleme20bN  40770  cdleme20c  40771  cdleme22aa  40799  cdleme22d  40803  cdleme22e  40804  cdleme27cl  40826  cdleme27a  40827  cdleme30a  40838  cdleme42a  40931  cdleme42c  40932  cdlemg2fv2  41060  cdlemg2m  41064  cdlemg4g  41076  cdlemg4  41077  cdlemg6c  41080  cdlemg7aN  41085  cdlemg9a  41092  cdlemg9b  41093  cdlemg10c  41099  cdlemg12a  41103  cdlemg12b  41104  cdlemg17a  41121  cdlemg18b  41139  cdlemg18c  41140  trlcoabs2N  41182  trlcolem  41186  tendoco2  41228  tendoicl  41256  cdlemi1  41278  cdlemi2  41279  cdlemj3  41283  tendocan  41284  cdlemk3  41293  cdlemk4  41294  cdlemk5a  41295  cdlemk9  41299  cdlemk9bN  41300  cdlemk10  41303  cdlemk30  41354  cdlemk31  41356  cdlemk39  41376  cdlemkfid1N  41381  cdlemkfid2N  41383  cdlemk19ylem  41390  cdlemk19xlem  41402  cdlemk53b  41416  cdlemk53  41417  cdlemk55a  41419  cdlemk43N  41423  cdlemk19u1  41429  cdlemm10N  41578  cdlemn2  41655  cdlemn10  41666  dihjustlem  41676  dihord2cN  41681  dihvalcq2  41707  dihopelvalcpre  41708  dihord5b  41719  dihord6b  41720  dihmeetlem2N  41759  dihmeetbclemN  41764  dihmeetlem4preN  41766  dihmeetALTN  41787  dochshpncl  41844  dochsatshpb  41912  hdmapval3N  42298  hgmap11  42362  f1o2d2  42688  remulcand  42885  pellfundex  43332  congtr  43411  fzmaxdif  43427  isnumbasgrplem2  43550  idomsubgmo  43639  ntrclsk13  44516  grumnudlem  44730  restuni3  45566  unirnmapsn  45661  ssmapsn  45663  infnsuprnmpt  45697  upbdrech  45756  suplesup  45787  infleinf  45819  supxrunb3  45846  mullimc  46064  islptre  46067  mullimcf  46071  neglimc  46093  limsupmnfuzlem  46172  limsupre3lem  46178  limsupre3uzlem  46181  icccncfext  46333  dvmptfprod  46391  stoweidlem31  46477  opnvonmbllem2  47079  smflimsuplem7  47272  ormkglobd  47321  funressneu  47507  cfsetsnfsetf1  47519  prmdvdsfmtnof1lem1  48059  uhgrimisgrgriclem  48418  clnbgrgrim  48422  grlimedgclnbgr  48483  domnmsuppn0  48857  lincext3  48944  2arymaptfo  49142