Theorem simp1r 1196

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

Syntax hints:   → wi 4   ∧ wa 395   ∧ w3a 1085

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 396  df-3an 1087

This theorem is referenced by:  simp11r  1283  simp21r  1289  simp31r  1295  offsplitfpar  7931  omeulem2  8376  uniinqs  8544  unxpdomlem3  8958  elfiun  9119  cofsmo  9956  isfin2-2  10006  isf32lem9  10048  tskun  10473  tskurn  10476  reclem3pr  10736  dedekind  11068  subaddmulsub  11368  dmdcan  11615  lt2msq1  11789  supmullem1  11875  supmul  11877  xaddass2  12913  xlt2add  12923  xmulasslem3  12949  iccsplit  13146  expaddzlem  13754  expaddz  13755  expmulz  13757  limsupgle  15114  o1add  15251  o1mul  15252  o1sub  15253  bitsfzo  16070  sadfval  16087  smufval  16112  prmexpb  16353  4sqlem18  16591  vdwlem10  16619  setsstruct2  16803  mrieqv2d  17265  curf1  17859  mgmsscl  18246  mndodcong  19065  subgabl  19352  gex2abl  19367  cntzsubr  19972  abvres  20014  lbsind2  20258  lbsextlem2  20336  lbsextg  20339  matring  21500  mdetunilem8  21676  maducoeval  21696  maducoeval2  21697  madurid  21701  cramerimplem3  21742  pmatcollpw2  21835  pm2mpf1  21856  cnprest  22348  isreg2  22436  fbssfi  22896  hausflimlem  23038  tmdgsum  23154  ssblps  23483  ssbl  23484  xrsmopn  23881  cphassi  24283  cphassir  24284  4cphipval2  24311  cphipval  24312  dvres2  24981  vieta1  25377  aalioulem4  25400  efgh  25602  cxpadd  25739  cxpsub  25742  divcxp  25747  cxple2  25757  cxplt2  25758  cxpcn3lem  25805  angcan  25857  ang180lem5  25868  isosctrlem3  25875  lgssq  26390  brbtwn2  27176  axcontlem4  27238  axcontlem8  27242  uhgr2edg  27478  chscllem4  29903  cshwrnid  31135  ogrpinvlt  31251  pstmval  31747  measinblem  32088  cvmlift2lem6  33170  eqfunresadj  33641  poseq  33729  nosupinfsep  33862  noetalem1  33871  noeta2  33906  sltlpss  34014  linethru  34382  cnres2  35848  lcv1  36982  lfl1  37011  lshpkrex  37059  hlrelat3  37353  cvrval3  37354  cvrval4N  37355  athgt  37397  atcvrlln2  37460  atcvrlln  37461  lvolnle3at  37523  lvolnlelpln  37526  4atlem11  37550  4atlem12  37553  2lplnj  37561  dalemddea  37625  cdlema2N  37733  paddasslem2  37762  atmod1i1m  37799  lhp2lt  37942  lhp0lt  37944  lhpexle3lem  37952  lhpj1  37963  lhpmcvr4N  37967  lhpelim  37978  lhpmod2i2  37979  lhpmod6i1  37980  cdlemb2  37982  lhpat  37984  ltrnatb  38078  ltrnel  38080  ltrncnvel  38083  ltrncnv  38087  trlval2  38104  trljat1  38107  trljat2  38108  trlnidatb  38118  cdlemc1  38132  cdlemc2  38133  cdlemc5  38136  cdlemc6  38137  cdleme0aa  38151  cdleme0b  38153  cdleme0c  38154  cdleme0e  38158  cdleme0fN  38159  cdleme01N  38162  cdleme0ex1N  38164  cdleme0moN  38166  cdleme3g  38175  cdleme3h  38176  cdleme3  38178  cdleme4  38179  cdleme4a  38180  cdleme5  38181  cdleme8  38191  cdleme9  38194  cdleme10  38195  cdleme16aN  38200  cdleme11fN  38205  cdleme11g  38206  cdleme11k  38209  cdleme13  38213  cdleme17c  38229  cdleme17d1  38230  cdleme18c  38234  cdleme22gb  38235  cdlemeda  38239  cdlemednpq  38240  cdlemednuN  38241  cdleme19c  38246  cdleme20aN  38250  cdleme20bN  38251  cdleme20c  38252  cdleme22aa  38280  cdleme22d  38284  cdleme22e  38285  cdleme27cl  38307  cdleme27a  38308  cdleme30a  38319  cdleme42a  38412  cdleme42c  38413  cdlemg2fv2  38541  cdlemg2m  38545  cdlemg4g  38557  cdlemg4  38558  cdlemg6c  38561  cdlemg7aN  38566  cdlemg9a  38573  cdlemg9b  38574  cdlemg10c  38580  cdlemg12a  38584  cdlemg12b  38585  cdlemg17a  38602  cdlemg18b  38620  cdlemg18c  38621  trlcoabs2N  38663  trlcolem  38667  tendoco2  38709  tendoicl  38737  cdlemi1  38759  cdlemi2  38760  cdlemj3  38764  tendocan  38765  cdlemk3  38774  cdlemk4  38775  cdlemk5a  38776  cdlemk9  38780  cdlemk9bN  38781  cdlemk10  38784  cdlemk30  38835  cdlemk31  38837  cdlemk39  38857  cdlemkfid1N  38862  cdlemkfid2N  38864  cdlemk19ylem  38871  cdlemk19xlem  38883  cdlemk53b  38897  cdlemk53  38898  cdlemk55a  38900  cdlemk43N  38904  cdlemk19u1  38910  cdlemm10N  39059  cdlemn2  39136  cdlemn10  39147  dihjustlem  39157  dihord2cN  39162  dihvalcq2  39188  dihopelvalcpre  39189  dihord5b  39200  dihord6b  39201  dihmeetlem2N  39240  dihmeetbclemN  39245  dihmeetlem4preN  39247  dihmeetALTN  39268  dochshpncl  39325  dochsatshpb  39393  hdmapval3N  39779  hgmap11  39843  nn0rppwr  40254  remulcand  40341  pellfundex  40624  congtr  40703  fzmaxdif  40719  isnumbasgrplem2  40845  idomsubgmo  40939  ntrclsk13  41570  grumnudlem  41792  restuni3  42556  unirnmapsn  42643  ssmapsn  42645  infnsuprnmpt  42685  upbdrech  42734  suplesup  42768  infleinf  42801  supxrunb3  42829  mullimc  43047  islptre  43050  mullimcf  43054  neglimc  43078  limsupmnfuzlem  43157  limsupre3lem  43163  limsupre3uzlem  43166  icccncfext  43318  dvmptfprod  43376  stoweidlem31  43462  opnvonmbllem2  44061  smflimsuplem7  44246  funressneu  44428  cfsetsnfsetf1  44440  prmdvdsfmtnof1lem1  44924  domnmsuppn0  45593  mndpfsupp  45600  lincext3  45685  2arymaptfo  45888