Theorem simp1r 1197

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 485	. 2 ⊢ ((𝜑 ∧ 𝜓) → 𝜓)
2	1	3ad2ant1 1132	1 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒 ∧ 𝜃) → 𝜓)

Syntax hints:   → wi 4   ∧ wa 396   ∧ w3a 1086

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 206  df-an 397  df-3an 1088

This theorem is referenced by:  simp11r  1284  simp21r  1290  simp31r  1296  offsplitfpar  7969  omeulem2  8423  uniinqs  8595  unxpdomlem3  9038  elfiun  9198  cofsmo  10034  isfin2-2  10084  isf32lem9  10126  tskun  10551  tskurn  10554  reclem3pr  10814  dedekind  11147  subaddmulsub  11447  dmdcan  11694  lt2msq1  11868  supmullem1  11954  supmul  11956  xaddass2  12993  xlt2add  13003  xmulasslem3  13029  iccsplit  13226  expaddzlem  13835  expaddz  13836  expmulz  13838  limsupgle  15195  o1add  15332  o1mul  15333  o1sub  15334  bitsfzo  16151  sadfval  16168  smufval  16193  prmexpb  16434  4sqlem18  16672  vdwlem10  16700  setsstruct2  16884  mrieqv2d  17357  curf1  17952  mgmsscl  18340  mndodcong  19159  subgabl  19446  gex2abl  19461  cntzsubr  20066  abvres  20108  lbsind2  20352  lbsextlem2  20430  lbsextg  20433  matring  21601  mdetunilem8  21777  maducoeval  21797  maducoeval2  21798  madurid  21802  cramerimplem3  21843  pmatcollpw2  21936  pm2mpf1  21957  cnprest  22449  isreg2  22537  fbssfi  22997  hausflimlem  23139  tmdgsum  23255  ssblps  23584  ssbl  23585  xrsmopn  23984  cphassi  24387  cphassir  24388  4cphipval2  24415  cphipval  24416  dvres2  25085  vieta1  25481  aalioulem4  25504  efgh  25706  cxpadd  25843  cxpsub  25846  divcxp  25851  cxple2  25861  cxplt2  25862  cxpcn3lem  25909  angcan  25961  ang180lem5  25972  isosctrlem3  25979  lgssq  26494  brbtwn2  27282  axcontlem4  27344  axcontlem8  27348  uhgr2edg  27584  chscllem4  30011  cshwrnid  31242  ogrpinvlt  31358  pstmval  31854  measinblem  32197  cvmlift2lem6  33279  eqfunresadj  33744  poseq  33811  nosupinfsep  33944  noetalem1  33953  noeta2  33988  sltlpss  34096  linethru  34464  cnres2  35930  lcv1  37062  lfl1  37091  lshpkrex  37139  hlrelat3  37433  cvrval3  37434  cvrval4N  37435  athgt  37477  atcvrlln2  37540  atcvrlln  37541  lvolnle3at  37603  lvolnlelpln  37606  4atlem11  37630  4atlem12  37633  2lplnj  37641  dalemddea  37705  cdlema2N  37813  paddasslem2  37842  atmod1i1m  37879  lhp2lt  38022  lhp0lt  38024  lhpexle3lem  38032  lhpj1  38043  lhpmcvr4N  38047  lhpelim  38058  lhpmod2i2  38059  lhpmod6i1  38060  cdlemb2  38062  lhpat  38064  ltrnatb  38158  ltrnel  38160  ltrncnvel  38163  ltrncnv  38167  trlval2  38184  trljat1  38187  trljat2  38188  trlnidatb  38198  cdlemc1  38212  cdlemc2  38213  cdlemc5  38216  cdlemc6  38217  cdleme0aa  38231  cdleme0b  38233  cdleme0c  38234  cdleme0e  38238  cdleme0fN  38239  cdleme01N  38242  cdleme0ex1N  38244  cdleme0moN  38246  cdleme3g  38255  cdleme3h  38256  cdleme3  38258  cdleme4  38259  cdleme4a  38260  cdleme5  38261  cdleme8  38271  cdleme9  38274  cdleme10  38275  cdleme16aN  38280  cdleme11fN  38285  cdleme11g  38286  cdleme11k  38289  cdleme13  38293  cdleme17c  38309  cdleme17d1  38310  cdleme18c  38314  cdleme22gb  38315  cdlemeda  38319  cdlemednpq  38320  cdlemednuN  38321  cdleme19c  38326  cdleme20aN  38330  cdleme20bN  38331  cdleme20c  38332  cdleme22aa  38360  cdleme22d  38364  cdleme22e  38365  cdleme27cl  38387  cdleme27a  38388  cdleme30a  38399  cdleme42a  38492  cdleme42c  38493  cdlemg2fv2  38621  cdlemg2m  38625  cdlemg4g  38637  cdlemg4  38638  cdlemg6c  38641  cdlemg7aN  38646  cdlemg9a  38653  cdlemg9b  38654  cdlemg10c  38660  cdlemg12a  38664  cdlemg12b  38665  cdlemg17a  38682  cdlemg18b  38700  cdlemg18c  38701  trlcoabs2N  38743  trlcolem  38747  tendoco2  38789  tendoicl  38817  cdlemi1  38839  cdlemi2  38840  cdlemj3  38844  tendocan  38845  cdlemk3  38854  cdlemk4  38855  cdlemk5a  38856  cdlemk9  38860  cdlemk9bN  38861  cdlemk10  38864  cdlemk30  38915  cdlemk31  38917  cdlemk39  38937  cdlemkfid1N  38942  cdlemkfid2N  38944  cdlemk19ylem  38951  cdlemk19xlem  38963  cdlemk53b  38977  cdlemk53  38978  cdlemk55a  38980  cdlemk43N  38984  cdlemk19u1  38990  cdlemm10N  39139  cdlemn2  39216  cdlemn10  39227  dihjustlem  39237  dihord2cN  39242  dihvalcq2  39268  dihopelvalcpre  39269  dihord5b  39280  dihord6b  39281  dihmeetlem2N  39320  dihmeetbclemN  39325  dihmeetlem4preN  39327  dihmeetALTN  39348  dochshpncl  39405  dochsatshpb  39473  hdmapval3N  39859  hgmap11  39923  nn0rppwr  40340  remulcand  40427  pellfundex  40715  congtr  40794  fzmaxdif  40810  isnumbasgrplem2  40936  idomsubgmo  41030  ntrclsk13  41688  grumnudlem  41910  restuni3  42674  unirnmapsn  42761  ssmapsn  42763  infnsuprnmpt  42803  upbdrech  42851  suplesup  42885  infleinf  42918  supxrunb3  42946  mullimc  43164  islptre  43167  mullimcf  43171  neglimc  43195  limsupmnfuzlem  43274  limsupre3lem  43280  limsupre3uzlem  43283  icccncfext  43435  dvmptfprod  43493  stoweidlem31  43579  opnvonmbllem2  44178  smflimsuplem7  44370  funressneu  44552  cfsetsnfsetf1  44564  prmdvdsfmtnof1lem1  45047  domnmsuppn0  45716  mndpfsupp  45723  lincext3  45808  2arymaptfo  46011