Theorem simp1r 1215

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

Syntax hints:   → wi 4   ∧ wa 400   ∧ w3a 1101

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 210  df-an 401  df-3an 1103

This theorem is referenced by:  simp11r  1302  simp21r  1308  simp31r  1314  eqfunresadj  7348  offsplitfpar  8102  mpof1o2d  8109  poseq  8142  omeulem2  8556  uniinqs  8783  unxpdomlem3  9206  elfiun  9378  cofsmo  10241  isfin2-2  10291  isf32lem9  10333  tskun  10759  tskurn  10762  reclem3pr  11022  dedekind  11361  subaddmulsub  11665  dmdcan  11916  lt2msq1  12090  supmullem1  12176  supmul  12178  xaddass2  13267  xlt2add  13277  xmulasslem3  13303  iccsplit  13503  expaddzlem  14132  expaddz  14133  expmulz  14135  limsupgle  15518  o1add  15655  o1mul  15656  o1sub  15657  bitsfzo  16483  sadfval  16500  smufval  16525  nn0rppwr  16609  prmexpb  16768  4sqlem18  17012  vdwlem10  17040  setsstruct2  17224  mrieqv2d  17685  curf1  18271  chnccat  18672  mgmsscl  18693  mndpfsupp  18815  mndodcong  19603  subgabl  19897  gex2abl  19912  ogrpinvlt  20205  rng1zrlem  20250  cntzsubrng  20643  cntzsubr  20682  abvres  20903  lbsind2  21171  lbsextlem2  21252  lbsextg  21255  matring  22561  mdetunilem8  22737  maducoeval  22757  maducoeval2  22758  madurid  22762  cramerimplem3  22803  pmatcollpw2  22896  pm2mpf1  22917  cnprest  23407  isreg2  23495  fbssfi  23955  hausflimlem  24097  tmdgsum  24213  ssblps  24540  ssbl  24541  xrsmopn  24931  cphassi  25334  cphassir  25335  4cphipval2  25362  cphipval  25363  dvres2  26032  vieta1  26434  aalioulem4  26457  efgh  26664  cxpadd  26802  cxpsub  26805  divcxp  26810  cxple2  26820  cxplt2  26821  cxpcn3lem  26870  angcan  26925  ang180lem5  26936  isosctrlem3  26943  lgssq  27459  nosupinfsep  27854  noetalem1  27863  noeta2  27912  ltslpss  28059  bdayfinbndlem1  28618  brbtwn2  29164  axcontlem4  29226  axcontlem8  29230  uhgr2edg  29467  chscllem4  31901  cshwrnid  33194  pstmval  34202  measinblem  34527  cvmlift2lem6  35671  linethru  36516  cnres2  38274  lcv1  39677  lfl1  39706  lshpkrex  39754  hlrelat3  40048  cvrval3  40049  cvrval4N  40050  athgt  40092  atcvrlln2  40155  atcvrlln  40156  lvolnle3at  40218  lvolnlelpln  40221  4atlem11  40245  4atlem12  40248  2lplnj  40256  dalemddea  40320  cdlema2N  40428  paddasslem2  40457  atmod1i1m  40494  lhp2lt  40637  lhp0lt  40639  lhpexle3lem  40647  lhpj1  40658  lhpmcvr4N  40662  lhpelim  40673  lhpmod2i2  40674  lhpmod6i1  40675  cdlemb2  40677  lhpat  40679  ltrnatb  40773  ltrnel  40775  ltrncnvel  40778  ltrncnv  40782  trlval2  40799  trljat1  40802  trljat2  40803  trlnidatb  40813  cdlemc1  40827  cdlemc2  40828  cdlemc5  40831  cdlemc6  40832  cdleme0aa  40846  cdleme0b  40848  cdleme0c  40849  cdleme0e  40853  cdleme0fN  40854  cdleme01N  40857  cdleme0ex1N  40859  cdleme0moN  40861  cdleme3g  40870  cdleme3h  40871  cdleme3  40873  cdleme4  40874  cdleme4a  40875  cdleme5  40876  cdleme8  40886  cdleme9  40889  cdleme10  40890  cdleme16aN  40895  cdleme11fN  40900  cdleme11g  40901  cdleme11k  40904  cdleme13  40908  cdleme17c  40924  cdleme17d1  40925  cdleme18c  40929  cdleme22gb  40930  cdlemeda  40934  cdlemednpq  40935  cdlemednuN  40936  cdleme19c  40941  cdleme20aN  40945  cdleme20bN  40946  cdleme20c  40947  cdleme22aa  40975  cdleme22d  40979  cdleme22e  40980  cdleme27cl  41002  cdleme27a  41003  cdleme30a  41014  cdleme42a  41107  cdleme42c  41108  cdlemg2fv2  41236  cdlemg2m  41240  cdlemg4g  41252  cdlemg4  41253  cdlemg6c  41256  cdlemg7aN  41261  cdlemg9a  41268  cdlemg9b  41269  cdlemg10c  41275  cdlemg12a  41279  cdlemg12b  41280  cdlemg17a  41297  cdlemg18b  41315  cdlemg18c  41316  trlcoabs2N  41358  trlcolem  41362  tendoco2  41404  tendoicl  41432  cdlemi1  41454  cdlemi2  41455  cdlemj3  41459  tendocan  41460  cdlemk3  41469  cdlemk4  41470  cdlemk5a  41471  cdlemk9  41475  cdlemk9bN  41476  cdlemk10  41479  cdlemk30  41530  cdlemk31  41532  cdlemk39  41552  cdlemkfid1N  41557  cdlemkfid2N  41559  cdlemk19ylem  41566  cdlemk19xlem  41578  cdlemk53b  41592  cdlemk53  41593  cdlemk55a  41595  cdlemk43N  41599  cdlemk19u1  41605  cdlemm10N  41754  cdlemn2  41831  cdlemn10  41842  dihjustlem  41852  dihord2cN  41857  dihvalcq2  41883  dihopelvalcpre  41884  dihord5b  41895  dihord6b  41896  dihmeetlem2N  41935  dihmeetbclemN  41940  dihmeetlem4preN  41942  dihmeetALTN  41963  dochshpncl  42020  dochsatshpb  42088  hdmapval3N  42474  hgmap11  42538  remulcand  43060  pellfundex  43475  congtr  43554  fzmaxdif  43570  isnumbasgrplem2  43693  idomsubgmo  43782  ntrclsk13  44659  grumnudlem  44859  restuni3  45694  unirnmapsn  45788  ssmapsn  45790  infnsuprnmpt  45823  upbdrech  45882  suplesup  45913  infleinf  45945  supxrunb3  45972  mullimc  46190  islptre  46193  mullimcf  46197  neglimc  46219  limsupmnfuzlem  46298  limsupre3lem  46304  limsupre3uzlem  46307  icccncfext  46459  dvmptfprod  46517  stoweidlem31  46603  opnvonmbllem2  47205  smflimsuplem7  47398  ormkglobd  47449  funressneu  47639  cfsetsnfsetf1  47651  prmdvdsfmtnof1lem1  48191  uhgrimisgrgriclem  48550  clnbgrgrim  48554  grlimedgclnbgr  48615  domnmsuppn0  49000  lincext3  49087  2arymaptfo  49285