Theorem simp1r 1217

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∧ w3a 1103

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105

This theorem is used by:  simp11r  1304  simp21r  1310  simp31r  1316  eqfunresadj  7367  offsplitfpar  8120  mpof1o2d  8127  poseq  8160  omeulem2  8574  uniinqs  8801  unxpdomlem3  9232  elfiun  9404  cofsmo  10275  isfin2-2  10325  isf32lem9  10367  tskun  10799  tskurn  10802  reclem3pr  11062  dedekind  11401  subaddmulsub  11705  dmdcan  11953  lt2msq1  12127  supmullem1  12213  supmul  12215  xaddass2  13306  xlt2add  13316  xmulasslem3  13342  iccsplit  13542  expaddzlem  14173  expaddz  14174  expmulz  14176  limsupgle  15568  o1add  15705  o1mul  15706  o1sub  15707  bitsfzo  16531  sadfval  16548  smufval  16573  nn0rppwr  16657  prmexpb  16816  4sqlem18  17060  vdwlem10  17088  setsstruct2  17272  mrieqv2d  17733  curf1  18319  chnccat  18720  mgmsscl  18741  mndpfsupp  18880  mndodcong  19675  subgabl  19969  gex2abl  19984  ogrpinvlt  20277  rng1zrlem  20322  cntzsubrng  20735  cntzsubr  20774  abvres  21003  lbsind2  21271  lbsextlem2  21352  lbsextg  21355  matring  22671  mdetunilem8  22847  maducoeval  22867  maducoeval2  22868  madurid  22872  cramerimplem3  22916  pmatcollpw2  23009  pm2mpf1  23030  cnprest  23520  isreg2  23608  fbssfi  24069  hausflimlem  24211  tmdgsum  24327  ssblps  24654  ssbl  24655  xrsmopn  25045  cphassi  25448  cphassir  25449  4cphipval2  25476  cphipval  25477  dvres2  26146  vieta1  26551  aalioulem4  26578  efgh  26786  cxpadd  26924  cxpsub  26927  divcxp  26932  cxple2  26942  cxplt2  26943  cxpcn3lem  26992  angcan  27047  ang180lem5  27058  isosctrlem3  27065  lgssq  27581  nosupinfsep  27976  noetalem1  27985  noeta2  28034  ltslpss  28181  bdayfinbndlem1  28740  brbtwn2  29370  axcontlem4  29432  axcontlem8  29436  uhgr2edg  29676  chscllem4  32129  cshwrnid  33409  pstmval  34413  measinblem  34739  cvmlift2lem6  35895  linethru  36741  cnres2  38521  lcv1  39922  lfl1  39951  lshpkrex  39999  hlrelat3  40293  cvrval3  40294  cvrval4N  40295  athgt  40337  atcvrlln2  40400  atcvrlln  40401  lvolnle3at  40463  lvolnlelpln  40466  4atlem11  40490  4atlem12  40493  2lplnj  40501  dalemddea  40565  cdlema2N  40673  paddasslem2  40702  atmod1i1m  40739  lhp2lt  40882  lhp0lt  40884  lhpexle3lem  40892  lhpj1  40903  lhpmcvr4N  40907  lhpelim  40918  lhpmod2i2  40919  lhpmod6i1  40920  cdlemb2  40922  lhpat  40924  ltrnatb  41018  ltrnel  41020  ltrncnvel  41023  ltrncnv  41027  trlval2  41044  trljat1  41047  trljat2  41048  trlnidatb  41058  cdlemc1  41072  cdlemc2  41073  cdlemc5  41076  cdlemc6  41077  cdleme0aa  41091  cdleme0b  41093  cdleme0c  41094  cdleme0e  41098  cdleme0fN  41099  cdleme01N  41102  cdleme0ex1N  41104  cdleme0moN  41106  cdleme3g  41115  cdleme3h  41116  cdleme3  41118  cdleme4  41119  cdleme4a  41120  cdleme5  41121  cdleme8  41131  cdleme9  41134  cdleme10  41135  cdleme16aN  41140  cdleme11fN  41145  cdleme11g  41146  cdleme11k  41149  cdleme13  41153  cdleme17c  41169  cdleme17d1  41170  cdleme18c  41174  cdleme22gb  41175  cdlemeda  41179  cdlemednpq  41180  cdlemednuN  41181  cdleme19c  41186  cdleme20aN  41190  cdleme20bN  41191  cdleme20c  41192  cdleme22aa  41220  cdleme22d  41224  cdleme22e  41225  cdleme27cl  41247  cdleme27a  41248  cdleme30a  41259  cdleme42a  41352  cdleme42c  41353  cdlemg2fv2  41481  cdlemg2m  41485  cdlemg4g  41497  cdlemg4  41498  cdlemg6c  41501  cdlemg7aN  41506  cdlemg9a  41513  cdlemg9b  41514  cdlemg10c  41520  cdlemg12a  41524  cdlemg12b  41525  cdlemg17a  41542  cdlemg18b  41560  cdlemg18c  41561  trlcoabs2N  41603  trlcolem  41607  tendoco2  41649  tendoicl  41677  cdlemi1  41699  cdlemi2  41700  cdlemj3  41704  tendocan  41705  cdlemk3  41714  cdlemk4  41715  cdlemk5a  41716  cdlemk9  41720  cdlemk9bN  41721  cdlemk10  41724  cdlemk30  41775  cdlemk31  41777  cdlemk39  41797  cdlemkfid1N  41802  cdlemkfid2N  41804  cdlemk19ylem  41811  cdlemk19xlem  41823  cdlemk53b  41837  cdlemk53  41838  cdlemk55a  41840  cdlemk43N  41844  cdlemk19u1  41850  cdlemm10N  41999  cdlemn2  42076  cdlemn10  42087  dihjustlem  42097  dihord2cN  42102  dihvalcq2  42128  dihopelvalcpre  42129  dihord5b  42140  dihord6b  42141  dihmeetlem2N  42180  dihmeetbclemN  42185  dihmeetlem4preN  42187  dihmeetALTN  42208  dochshpncl  42265  dochsatshpb  42333  hdmapval3N  42719  hgmap11  42783  remulcand  43322  pellfundex  43735  congtr  43814  fzmaxdif  43830  isnumbasgrplem2  43953  idomsubgmo  44042  ntrclsk13  44919  grumnudlem  45117  restuni3  45958  unirnmapsn  46052  ssmapsn  46054  infnsuprnmpt  46087  upbdrech  46146  suplesup  46177  infleinf  46209  supxrunb3  46236  mullimc  46454  islptre  46457  mullimcf  46461  neglimc  46483  limsupmnfuzlem  46562  limsupre3lem  46568  limsupre3uzlem  46571  icccncfext  46723  dvmptfprod  46781  stoweidlem31  46867  opnvonmbllem2  47469  smflimsuplem7  47662  ormkglobd  47713  funressneu  47943  cfsetsnfsetf1  47955  prmdvdsfmtnof1lem1  48495  uhgrimisgrgriclem  48854  clnbgrgrim  48858  grlimedgclnbgr  48919  domnmsuppn0  49307  lincext3  49394  2arymaptfo  49592