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  7951  omeulem2  8399  uniinqs  8569  unxpdomlem3  9007  elfiun  9167  cofsmo  10026  isfin2-2  10076  isf32lem9  10118  tskun  10543  tskurn  10546  reclem3pr  10806  dedekind  11138  subaddmulsub  11438  dmdcan  11685  lt2msq1  11859  supmullem1  11945  supmul  11947  xaddass2  12983  xlt2add  12993  xmulasslem3  13019  iccsplit  13216  expaddzlem  13824  expaddz  13825  expmulz  13827  limsupgle  15184  o1add  15321  o1mul  15322  o1sub  15323  bitsfzo  16140  sadfval  16157  smufval  16182  prmexpb  16423  4sqlem18  16661  vdwlem10  16689  setsstruct2  16873  mrieqv2d  17346  curf1  17941  mgmsscl  18329  mndodcong  19148  subgabl  19435  gex2abl  19450  cntzsubr  20055  abvres  20097  lbsind2  20341  lbsextlem2  20419  lbsextg  20422  matring  21590  mdetunilem8  21766  maducoeval  21786  maducoeval2  21787  madurid  21791  cramerimplem3  21832  pmatcollpw2  21925  pm2mpf1  21946  cnprest  22438  isreg2  22526  fbssfi  22986  hausflimlem  23128  tmdgsum  23244  ssblps  23573  ssbl  23574  xrsmopn  23973  cphassi  24376  cphassir  24377  4cphipval2  24404  cphipval  24405  dvres2  25074  vieta1  25470  aalioulem4  25493  efgh  25695  cxpadd  25832  cxpsub  25835  divcxp  25840  cxple2  25850  cxplt2  25851  cxpcn3lem  25898  angcan  25950  ang180lem5  25961  isosctrlem3  25968  lgssq  26483  brbtwn2  27271  axcontlem4  27333  axcontlem8  27337  uhgr2edg  27573  chscllem4  29998  cshwrnid  31229  ogrpinvlt  31345  pstmval  31841  measinblem  32184  cvmlift2lem6  33266  eqfunresadj  33731  poseq  33798  nosupinfsep  33931  noetalem1  33940  noeta2  33975  sltlpss  34083  linethru  34451  cnres2  35917  lcv1  37051  lfl1  37080  lshpkrex  37128  hlrelat3  37422  cvrval3  37423  cvrval4N  37424  athgt  37466  atcvrlln2  37529  atcvrlln  37530  lvolnle3at  37592  lvolnlelpln  37595  4atlem11  37619  4atlem12  37622  2lplnj  37630  dalemddea  37694  cdlema2N  37802  paddasslem2  37831  atmod1i1m  37868  lhp2lt  38011  lhp0lt  38013  lhpexle3lem  38021  lhpj1  38032  lhpmcvr4N  38036  lhpelim  38047  lhpmod2i2  38048  lhpmod6i1  38049  cdlemb2  38051  lhpat  38053  ltrnatb  38147  ltrnel  38149  ltrncnvel  38152  ltrncnv  38156  trlval2  38173  trljat1  38176  trljat2  38177  trlnidatb  38187  cdlemc1  38201  cdlemc2  38202  cdlemc5  38205  cdlemc6  38206  cdleme0aa  38220  cdleme0b  38222  cdleme0c  38223  cdleme0e  38227  cdleme0fN  38228  cdleme01N  38231  cdleme0ex1N  38233  cdleme0moN  38235  cdleme3g  38244  cdleme3h  38245  cdleme3  38247  cdleme4  38248  cdleme4a  38249  cdleme5  38250  cdleme8  38260  cdleme9  38263  cdleme10  38264  cdleme16aN  38269  cdleme11fN  38274  cdleme11g  38275  cdleme11k  38278  cdleme13  38282  cdleme17c  38298  cdleme17d1  38299  cdleme18c  38303  cdleme22gb  38304  cdlemeda  38308  cdlemednpq  38309  cdlemednuN  38310  cdleme19c  38315  cdleme20aN  38319  cdleme20bN  38320  cdleme20c  38321  cdleme22aa  38349  cdleme22d  38353  cdleme22e  38354  cdleme27cl  38376  cdleme27a  38377  cdleme30a  38388  cdleme42a  38481  cdleme42c  38482  cdlemg2fv2  38610  cdlemg2m  38614  cdlemg4g  38626  cdlemg4  38627  cdlemg6c  38630  cdlemg7aN  38635  cdlemg9a  38642  cdlemg9b  38643  cdlemg10c  38649  cdlemg12a  38653  cdlemg12b  38654  cdlemg17a  38671  cdlemg18b  38689  cdlemg18c  38690  trlcoabs2N  38732  trlcolem  38736  tendoco2  38778  tendoicl  38806  cdlemi1  38828  cdlemi2  38829  cdlemj3  38833  tendocan  38834  cdlemk3  38843  cdlemk4  38844  cdlemk5a  38845  cdlemk9  38849  cdlemk9bN  38850  cdlemk10  38853  cdlemk30  38904  cdlemk31  38906  cdlemk39  38926  cdlemkfid1N  38931  cdlemkfid2N  38933  cdlemk19ylem  38940  cdlemk19xlem  38952  cdlemk53b  38966  cdlemk53  38967  cdlemk55a  38969  cdlemk43N  38973  cdlemk19u1  38979  cdlemm10N  39128  cdlemn2  39205  cdlemn10  39216  dihjustlem  39226  dihord2cN  39231  dihvalcq2  39257  dihopelvalcpre  39258  dihord5b  39269  dihord6b  39270  dihmeetlem2N  39309  dihmeetbclemN  39314  dihmeetlem4preN  39316  dihmeetALTN  39337  dochshpncl  39394  dochsatshpb  39462  hdmapval3N  39848  hgmap11  39912  nn0rppwr  40330  remulcand  40417  pellfundex  40705  congtr  40784  fzmaxdif  40800  isnumbasgrplem2  40926  idomsubgmo  41020  ntrclsk13  41651  grumnudlem  41873  restuni3  42637  unirnmapsn  42724  ssmapsn  42726  infnsuprnmpt  42766  upbdrech  42815  suplesup  42849  infleinf  42882  supxrunb3  42910  mullimc  43128  islptre  43131  mullimcf  43135  neglimc  43159  limsupmnfuzlem  43238  limsupre3lem  43244  limsupre3uzlem  43247  icccncfext  43399  dvmptfprod  43457  stoweidlem31  43543  opnvonmbllem2  44142  smflimsuplem7  44327  funressneu  44509  cfsetsnfsetf1  44521  prmdvdsfmtnof1lem1  45005  domnmsuppn0  45674  mndpfsupp  45681  lincext3  45766  2arymaptfo  45969