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  7352  offsplitfpar  8116  poseq  8155  omeulem2  8593  uniinqs  8809  unxpdomlem3  9258  elfiun  9440  cofsmo  10281  isfin2-2  10331  isf32lem9  10373  tskun  10798  tskurn  10801  reclem3pr  11061  dedekind  11396  subaddmulsub  11698  dmdcan  11949  lt2msq1  12124  supmullem1  12210  supmul  12212  xaddass2  13264  xlt2add  13274  xmulasslem3  13300  iccsplit  13500  expaddzlem  14121  expaddz  14122  expmulz  14124  limsupgle  15491  o1add  15628  o1mul  15629  o1sub  15630  bitsfzo  16452  sadfval  16469  smufval  16494  nn0rppwr  16578  prmexpb  16736  4sqlem18  16980  vdwlem10  17008  setsstruct2  17191  mrieqv2d  17649  curf1  18235  mgmsscl  18621  mndpfsupp  18743  mndodcong  19521  subgabl  19815  gex2abl  19830  cntzsubrng  20525  cntzsubr  20564  abvres  20789  lbsind2  21037  lbsextlem2  21118  lbsextg  21121  matring  22379  mdetunilem8  22555  maducoeval  22575  maducoeval2  22576  madurid  22580  cramerimplem3  22621  pmatcollpw2  22714  pm2mpf1  22735  cnprest  23225  isreg2  23313  fbssfi  23773  hausflimlem  23915  tmdgsum  24031  ssblps  24359  ssbl  24360  xrsmopn  24750  cphassi  25164  cphassir  25165  4cphipval2  25192  cphipval  25193  dvres2  25863  vieta1  26270  aalioulem4  26293  efgh  26500  cxpadd  26638  cxpsub  26641  divcxp  26646  cxple2  26656  cxplt2  26657  cxpcn3lem  26707  angcan  26762  ang180lem5  26773  isosctrlem3  26780  lgssq  27298  nosupinfsep  27694  noetalem1  27703  noeta2  27746  sltlpss  27862  brbtwn2  28830  axcontlem4  28892  axcontlem8  28896  uhgr2edg  29133  chscllem4  31567  cshwrnid  32883  ogrpinvlt  33037  pstmval  33872  measinblem  34197  cvmlift2lem6  35276  linethru  36117  cnres2  37733  lcv1  39005  lfl1  39034  lshpkrex  39082  hlrelat3  39377  cvrval3  39378  cvrval4N  39379  athgt  39421  atcvrlln2  39484  atcvrlln  39485  lvolnle3at  39547  lvolnlelpln  39550  4atlem11  39574  4atlem12  39577  2lplnj  39585  dalemddea  39649  cdlema2N  39757  paddasslem2  39786  atmod1i1m  39823  lhp2lt  39966  lhp0lt  39968  lhpexle3lem  39976  lhpj1  39987  lhpmcvr4N  39991  lhpelim  40002  lhpmod2i2  40003  lhpmod6i1  40004  cdlemb2  40006  lhpat  40008  ltrnatb  40102  ltrnel  40104  ltrncnvel  40107  ltrncnv  40111  trlval2  40128  trljat1  40131  trljat2  40132  trlnidatb  40142  cdlemc1  40156  cdlemc2  40157  cdlemc5  40160  cdlemc6  40161  cdleme0aa  40175  cdleme0b  40177  cdleme0c  40178  cdleme0e  40182  cdleme0fN  40183  cdleme01N  40186  cdleme0ex1N  40188  cdleme0moN  40190  cdleme3g  40199  cdleme3h  40200  cdleme3  40202  cdleme4  40203  cdleme4a  40204  cdleme5  40205  cdleme8  40215  cdleme9  40218  cdleme10  40219  cdleme16aN  40224  cdleme11fN  40229  cdleme11g  40230  cdleme11k  40233  cdleme13  40237  cdleme17c  40253  cdleme17d1  40254  cdleme18c  40258  cdleme22gb  40259  cdlemeda  40263  cdlemednpq  40264  cdlemednuN  40265  cdleme19c  40270  cdleme20aN  40274  cdleme20bN  40275  cdleme20c  40276  cdleme22aa  40304  cdleme22d  40308  cdleme22e  40309  cdleme27cl  40331  cdleme27a  40332  cdleme30a  40343  cdleme42a  40436  cdleme42c  40437  cdlemg2fv2  40565  cdlemg2m  40569  cdlemg4g  40581  cdlemg4  40582  cdlemg6c  40585  cdlemg7aN  40590  cdlemg9a  40597  cdlemg9b  40598  cdlemg10c  40604  cdlemg12a  40608  cdlemg12b  40609  cdlemg17a  40626  cdlemg18b  40644  cdlemg18c  40645  trlcoabs2N  40687  trlcolem  40691  tendoco2  40733  tendoicl  40761  cdlemi1  40783  cdlemi2  40784  cdlemj3  40788  tendocan  40789  cdlemk3  40798  cdlemk4  40799  cdlemk5a  40800  cdlemk9  40804  cdlemk9bN  40805  cdlemk10  40808  cdlemk30  40859  cdlemk31  40861  cdlemk39  40881  cdlemkfid1N  40886  cdlemkfid2N  40888  cdlemk19ylem  40895  cdlemk19xlem  40907  cdlemk53b  40921  cdlemk53  40922  cdlemk55a  40924  cdlemk43N  40928  cdlemk19u1  40934  cdlemm10N  41083  cdlemn2  41160  cdlemn10  41171  dihjustlem  41181  dihord2cN  41186  dihvalcq2  41212  dihopelvalcpre  41213  dihord5b  41224  dihord6b  41225  dihmeetlem2N  41264  dihmeetbclemN  41269  dihmeetlem4preN  41271  dihmeetALTN  41292  dochshpncl  41349  dochsatshpb  41417  hdmapval3N  41803  hgmap11  41867  f1o2d2  42231  remulcand  42428  pellfundex  42856  congtr  42936  fzmaxdif  42952  isnumbasgrplem2  43075  idomsubgmo  43164  ntrclsk13  44042  grumnudlem  44257  restuni3  45090  unirnmapsn  45186  ssmapsn  45188  infnsuprnmpt  45222  upbdrech  45282  suplesup  45314  infleinf  45347  supxrunb3  45374  mullimc  45593  islptre  45596  mullimcf  45600  neglimc  45624  limsupmnfuzlem  45703  limsupre3lem  45709  limsupre3uzlem  45712  icccncfext  45864  dvmptfprod  45922  stoweidlem31  46008  opnvonmbllem2  46610  smflimsuplem7  46803  ormkglobd  46852  funressneu  47024  cfsetsnfsetf1  47036  prmdvdsfmtnof1lem1  47546  uhgrimisgrgriclem  47891  clnbgrgrim  47895  domnmsuppn0  48292  lincext3  48380  2arymaptfo  48582