Theorem simp1r 1199

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 1133	1 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒 ∧ 𝜃) → 𝜓)

Syntax hints:   → wi 4   ∧ wa 395   ∧ 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 207  df-an 396  df-3an 1088

This theorem is referenced by:  simp11r  1286  simp21r  1292  simp31r  1298  eqfunresadj  7301  offsplitfpar  8059  poseq  8098  omeulem2  8508  uniinqs  8731  unxpdomlem3  9157  elfiun  9339  cofsmo  10182  isfin2-2  10232  isf32lem9  10274  tskun  10699  tskurn  10702  reclem3pr  10962  dedekind  11297  subaddmulsub  11601  dmdcan  11852  lt2msq1  12027  supmullem1  12113  supmul  12115  xaddass2  13170  xlt2add  13180  xmulasslem3  13206  iccsplit  13406  expaddzlem  14030  expaddz  14031  expmulz  14033  limsupgle  15402  o1add  15539  o1mul  15540  o1sub  15541  bitsfzo  16364  sadfval  16381  smufval  16406  nn0rppwr  16490  prmexpb  16648  4sqlem18  16892  vdwlem10  16920  setsstruct2  17103  mrieqv2d  17563  curf1  18149  mgmsscl  18537  mndpfsupp  18659  mndodcong  19439  subgabl  19733  gex2abl  19748  ogrpinvlt  20041  cntzsubrng  20470  cntzsubr  20509  abvres  20734  lbsind2  21003  lbsextlem2  21084  lbsextg  21087  matring  22346  mdetunilem8  22522  maducoeval  22542  maducoeval2  22543  madurid  22547  cramerimplem3  22588  pmatcollpw2  22681  pm2mpf1  22702  cnprest  23192  isreg2  23280  fbssfi  23740  hausflimlem  23882  tmdgsum  23998  ssblps  24326  ssbl  24327  xrsmopn  24717  cphassi  25130  cphassir  25131  4cphipval2  25158  cphipval  25159  dvres2  25829  vieta1  26236  aalioulem4  26259  efgh  26466  cxpadd  26604  cxpsub  26607  divcxp  26612  cxple2  26622  cxplt2  26623  cxpcn3lem  26673  angcan  26728  ang180lem5  26739  isosctrlem3  26746  lgssq  27264  nosupinfsep  27660  noetalem1  27669  noeta2  27713  sltlpss  27840  brbtwn2  28868  axcontlem4  28930  axcontlem8  28934  uhgr2edg  29171  chscllem4  31602  cshwrnid  32916  pstmval  33861  measinblem  34186  cvmlift2lem6  35280  linethru  36126  cnres2  37742  lcv1  39019  lfl1  39048  lshpkrex  39096  hlrelat3  39391  cvrval3  39392  cvrval4N  39393  athgt  39435  atcvrlln2  39498  atcvrlln  39499  lvolnle3at  39561  lvolnlelpln  39564  4atlem11  39588  4atlem12  39591  2lplnj  39599  dalemddea  39663  cdlema2N  39771  paddasslem2  39800  atmod1i1m  39837  lhp2lt  39980  lhp0lt  39982  lhpexle3lem  39990  lhpj1  40001  lhpmcvr4N  40005  lhpelim  40016  lhpmod2i2  40017  lhpmod6i1  40018  cdlemb2  40020  lhpat  40022  ltrnatb  40116  ltrnel  40118  ltrncnvel  40121  ltrncnv  40125  trlval2  40142  trljat1  40145  trljat2  40146  trlnidatb  40156  cdlemc1  40170  cdlemc2  40171  cdlemc5  40174  cdlemc6  40175  cdleme0aa  40189  cdleme0b  40191  cdleme0c  40192  cdleme0e  40196  cdleme0fN  40197  cdleme01N  40200  cdleme0ex1N  40202  cdleme0moN  40204  cdleme3g  40213  cdleme3h  40214  cdleme3  40216  cdleme4  40217  cdleme4a  40218  cdleme5  40219  cdleme8  40229  cdleme9  40232  cdleme10  40233  cdleme16aN  40238  cdleme11fN  40243  cdleme11g  40244  cdleme11k  40247  cdleme13  40251  cdleme17c  40267  cdleme17d1  40268  cdleme18c  40272  cdleme22gb  40273  cdlemeda  40277  cdlemednpq  40278  cdlemednuN  40279  cdleme19c  40284  cdleme20aN  40288  cdleme20bN  40289  cdleme20c  40290  cdleme22aa  40318  cdleme22d  40322  cdleme22e  40323  cdleme27cl  40345  cdleme27a  40346  cdleme30a  40357  cdleme42a  40450  cdleme42c  40451  cdlemg2fv2  40579  cdlemg2m  40583  cdlemg4g  40595  cdlemg4  40596  cdlemg6c  40599  cdlemg7aN  40604  cdlemg9a  40611  cdlemg9b  40612  cdlemg10c  40618  cdlemg12a  40622  cdlemg12b  40623  cdlemg17a  40640  cdlemg18b  40658  cdlemg18c  40659  trlcoabs2N  40701  trlcolem  40705  tendoco2  40747  tendoicl  40775  cdlemi1  40797  cdlemi2  40798  cdlemj3  40802  tendocan  40803  cdlemk3  40812  cdlemk4  40813  cdlemk5a  40814  cdlemk9  40818  cdlemk9bN  40819  cdlemk10  40822  cdlemk30  40873  cdlemk31  40875  cdlemk39  40895  cdlemkfid1N  40900  cdlemkfid2N  40902  cdlemk19ylem  40909  cdlemk19xlem  40921  cdlemk53b  40935  cdlemk53  40936  cdlemk55a  40938  cdlemk43N  40942  cdlemk19u1  40948  cdlemm10N  41097  cdlemn2  41174  cdlemn10  41185  dihjustlem  41195  dihord2cN  41200  dihvalcq2  41226  dihopelvalcpre  41227  dihord5b  41238  dihord6b  41239  dihmeetlem2N  41278  dihmeetbclemN  41283  dihmeetlem4preN  41285  dihmeetALTN  41306  dochshpncl  41363  dochsatshpb  41431  hdmapval3N  41817  hgmap11  41881  f1o2d2  42206  remulcand  42412  pellfundex  42859  congtr  42938  fzmaxdif  42954  isnumbasgrplem2  43077  idomsubgmo  43166  ntrclsk13  44044  grumnudlem  44258  restuni3  45096  unirnmapsn  45192  ssmapsn  45194  infnsuprnmpt  45228  upbdrech  45287  suplesup  45319  infleinf  45352  supxrunb3  45379  mullimc  45598  islptre  45601  mullimcf  45605  neglimc  45629  limsupmnfuzlem  45708  limsupre3lem  45714  limsupre3uzlem  45717  icccncfext  45869  dvmptfprod  45927  stoweidlem31  46013  opnvonmbllem2  46615  smflimsuplem7  46808  ormkglobd  46857  funressneu  47032  cfsetsnfsetf1  47044  prmdvdsfmtnof1lem1  47569  uhgrimisgrgriclem  47915  clnbgrgrim  47919  grlimedgclnbgr  47980  domnmsuppn0  48354  lincext3  48442  2arymaptfo  48640