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  7335  offsplitfpar  8098  poseq  8137  omeulem2  8547  uniinqs  8770  unxpdomlem3  9199  elfiun  9381  cofsmo  10222  isfin2-2  10272  isf32lem9  10314  tskun  10739  tskurn  10742  reclem3pr  11002  dedekind  11337  subaddmulsub  11641  dmdcan  11892  lt2msq1  12067  supmullem1  12153  supmul  12155  xaddass2  13210  xlt2add  13220  xmulasslem3  13246  iccsplit  13446  expaddzlem  14070  expaddz  14071  expmulz  14073  limsupgle  15443  o1add  15580  o1mul  15581  o1sub  15582  bitsfzo  16405  sadfval  16422  smufval  16447  nn0rppwr  16531  prmexpb  16689  4sqlem18  16933  vdwlem10  16961  setsstruct2  17144  mrieqv2d  17600  curf1  18186  mgmsscl  18572  mndpfsupp  18694  mndodcong  19472  subgabl  19766  gex2abl  19781  cntzsubrng  20476  cntzsubr  20515  abvres  20740  lbsind2  20988  lbsextlem2  21069  lbsextg  21072  matring  22330  mdetunilem8  22506  maducoeval  22526  maducoeval2  22527  madurid  22531  cramerimplem3  22572  pmatcollpw2  22665  pm2mpf1  22686  cnprest  23176  isreg2  23264  fbssfi  23724  hausflimlem  23866  tmdgsum  23982  ssblps  24310  ssbl  24311  xrsmopn  24701  cphassi  25114  cphassir  25115  4cphipval2  25142  cphipval  25143  dvres2  25813  vieta1  26220  aalioulem4  26243  efgh  26450  cxpadd  26588  cxpsub  26591  divcxp  26596  cxple2  26606  cxplt2  26607  cxpcn3lem  26657  angcan  26712  ang180lem5  26723  isosctrlem3  26730  lgssq  27248  nosupinfsep  27644  noetalem1  27653  noeta2  27696  sltlpss  27819  brbtwn2  28832  axcontlem4  28894  axcontlem8  28898  uhgr2edg  29135  chscllem4  31569  cshwrnid  32883  ogrpinvlt  33037  pstmval  33885  measinblem  34210  cvmlift2lem6  35295  linethru  36141  cnres2  37757  lcv1  39034  lfl1  39063  lshpkrex  39111  hlrelat3  39406  cvrval3  39407  cvrval4N  39408  athgt  39450  atcvrlln2  39513  atcvrlln  39514  lvolnle3at  39576  lvolnlelpln  39579  4atlem11  39603  4atlem12  39606  2lplnj  39614  dalemddea  39678  cdlema2N  39786  paddasslem2  39815  atmod1i1m  39852  lhp2lt  39995  lhp0lt  39997  lhpexle3lem  40005  lhpj1  40016  lhpmcvr4N  40020  lhpelim  40031  lhpmod2i2  40032  lhpmod6i1  40033  cdlemb2  40035  lhpat  40037  ltrnatb  40131  ltrnel  40133  ltrncnvel  40136  ltrncnv  40140  trlval2  40157  trljat1  40160  trljat2  40161  trlnidatb  40171  cdlemc1  40185  cdlemc2  40186  cdlemc5  40189  cdlemc6  40190  cdleme0aa  40204  cdleme0b  40206  cdleme0c  40207  cdleme0e  40211  cdleme0fN  40212  cdleme01N  40215  cdleme0ex1N  40217  cdleme0moN  40219  cdleme3g  40228  cdleme3h  40229  cdleme3  40231  cdleme4  40232  cdleme4a  40233  cdleme5  40234  cdleme8  40244  cdleme9  40247  cdleme10  40248  cdleme16aN  40253  cdleme11fN  40258  cdleme11g  40259  cdleme11k  40262  cdleme13  40266  cdleme17c  40282  cdleme17d1  40283  cdleme18c  40287  cdleme22gb  40288  cdlemeda  40292  cdlemednpq  40293  cdlemednuN  40294  cdleme19c  40299  cdleme20aN  40303  cdleme20bN  40304  cdleme20c  40305  cdleme22aa  40333  cdleme22d  40337  cdleme22e  40338  cdleme27cl  40360  cdleme27a  40361  cdleme30a  40372  cdleme42a  40465  cdleme42c  40466  cdlemg2fv2  40594  cdlemg2m  40598  cdlemg4g  40610  cdlemg4  40611  cdlemg6c  40614  cdlemg7aN  40619  cdlemg9a  40626  cdlemg9b  40627  cdlemg10c  40633  cdlemg12a  40637  cdlemg12b  40638  cdlemg17a  40655  cdlemg18b  40673  cdlemg18c  40674  trlcoabs2N  40716  trlcolem  40720  tendoco2  40762  tendoicl  40790  cdlemi1  40812  cdlemi2  40813  cdlemj3  40817  tendocan  40818  cdlemk3  40827  cdlemk4  40828  cdlemk5a  40829  cdlemk9  40833  cdlemk9bN  40834  cdlemk10  40837  cdlemk30  40888  cdlemk31  40890  cdlemk39  40910  cdlemkfid1N  40915  cdlemkfid2N  40917  cdlemk19ylem  40924  cdlemk19xlem  40936  cdlemk53b  40950  cdlemk53  40951  cdlemk55a  40953  cdlemk43N  40957  cdlemk19u1  40963  cdlemm10N  41112  cdlemn2  41189  cdlemn10  41200  dihjustlem  41210  dihord2cN  41215  dihvalcq2  41241  dihopelvalcpre  41242  dihord5b  41253  dihord6b  41254  dihmeetlem2N  41293  dihmeetbclemN  41298  dihmeetlem4preN  41300  dihmeetALTN  41321  dochshpncl  41378  dochsatshpb  41446  hdmapval3N  41832  hgmap11  41896  f1o2d2  42221  remulcand  42427  pellfundex  42874  congtr  42954  fzmaxdif  42970  isnumbasgrplem2  43093  idomsubgmo  43182  ntrclsk13  44060  grumnudlem  44274  restuni3  45112  unirnmapsn  45208  ssmapsn  45210  infnsuprnmpt  45244  upbdrech  45303  suplesup  45335  infleinf  45368  supxrunb3  45395  mullimc  45614  islptre  45617  mullimcf  45621  neglimc  45645  limsupmnfuzlem  45724  limsupre3lem  45730  limsupre3uzlem  45733  icccncfext  45885  dvmptfprod  45943  stoweidlem31  46029  opnvonmbllem2  46631  smflimsuplem7  46824  ormkglobd  46873  funressneu  47048  cfsetsnfsetf1  47060  prmdvdsfmtnof1lem1  47585  uhgrimisgrgriclem  47930  clnbgrgrim  47934  domnmsuppn0  48357  lincext3  48445  2arymaptfo  48643