Theorem simp1r 1200

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

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

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 1089

This theorem is referenced by:  simp11r  1287  simp21r  1293  simp31r  1299  eqfunresadj  7316  offsplitfpar  8071  poseq  8110  omeulem2  8520  uniinqs  8746  unxpdomlem3  9170  elfiun  9345  cofsmo  10191  isfin2-2  10241  isf32lem9  10283  tskun  10709  tskurn  10712  reclem3pr  10972  dedekind  11308  subaddmulsub  11612  dmdcan  11863  lt2msq1  12038  supmullem1  12124  supmul  12126  xaddass2  13177  xlt2add  13187  xmulasslem3  13213  iccsplit  13413  expaddzlem  14040  expaddz  14041  expmulz  14043  limsupgle  15412  o1add  15549  o1mul  15550  o1sub  15551  bitsfzo  16374  sadfval  16391  smufval  16416  nn0rppwr  16500  prmexpb  16658  4sqlem18  16902  vdwlem10  16930  setsstruct2  17113  mrieqv2d  17574  curf1  18160  chnccat  18561  mgmsscl  18582  mndpfsupp  18704  mndodcong  19483  subgabl  19777  gex2abl  19792  ogrpinvlt  20085  cntzsubrng  20512  cntzsubr  20551  abvres  20776  lbsind2  21045  lbsextlem2  21126  lbsextg  21129  matring  22399  mdetunilem8  22575  maducoeval  22595  maducoeval2  22596  madurid  22600  cramerimplem3  22641  pmatcollpw2  22734  pm2mpf1  22755  cnprest  23245  isreg2  23333  fbssfi  23793  hausflimlem  23935  tmdgsum  24051  ssblps  24378  ssbl  24379  xrsmopn  24769  cphassi  25182  cphassir  25183  4cphipval2  25210  cphipval  25211  dvres2  25881  vieta1  26288  aalioulem4  26311  efgh  26518  cxpadd  26656  cxpsub  26659  divcxp  26664  cxple2  26674  cxplt2  26675  cxpcn3lem  26725  angcan  26780  ang180lem5  26791  isosctrlem3  26798  lgssq  27316  nosupinfsep  27712  noetalem1  27721  noeta2  27769  ltslpss  27916  bdayfinbndlem1  28475  brbtwn2  28990  axcontlem4  29052  axcontlem8  29056  uhgr2edg  29293  chscllem4  31727  cshwrnid  33053  pstmval  34072  measinblem  34397  cvmlift2lem6  35521  linethru  36366  cnres2  38008  lcv1  39411  lfl1  39440  lshpkrex  39488  hlrelat3  39782  cvrval3  39783  cvrval4N  39784  athgt  39826  atcvrlln2  39889  atcvrlln  39890  lvolnle3at  39952  lvolnlelpln  39955  4atlem11  39979  4atlem12  39982  2lplnj  39990  dalemddea  40054  cdlema2N  40162  paddasslem2  40191  atmod1i1m  40228  lhp2lt  40371  lhp0lt  40373  lhpexle3lem  40381  lhpj1  40392  lhpmcvr4N  40396  lhpelim  40407  lhpmod2i2  40408  lhpmod6i1  40409  cdlemb2  40411  lhpat  40413  ltrnatb  40507  ltrnel  40509  ltrncnvel  40512  ltrncnv  40516  trlval2  40533  trljat1  40536  trljat2  40537  trlnidatb  40547  cdlemc1  40561  cdlemc2  40562  cdlemc5  40565  cdlemc6  40566  cdleme0aa  40580  cdleme0b  40582  cdleme0c  40583  cdleme0e  40587  cdleme0fN  40588  cdleme01N  40591  cdleme0ex1N  40593  cdleme0moN  40595  cdleme3g  40604  cdleme3h  40605  cdleme3  40607  cdleme4  40608  cdleme4a  40609  cdleme5  40610  cdleme8  40620  cdleme9  40623  cdleme10  40624  cdleme16aN  40629  cdleme11fN  40634  cdleme11g  40635  cdleme11k  40638  cdleme13  40642  cdleme17c  40658  cdleme17d1  40659  cdleme18c  40663  cdleme22gb  40664  cdlemeda  40668  cdlemednpq  40669  cdlemednuN  40670  cdleme19c  40675  cdleme20aN  40679  cdleme20bN  40680  cdleme20c  40681  cdleme22aa  40709  cdleme22d  40713  cdleme22e  40714  cdleme27cl  40736  cdleme27a  40737  cdleme30a  40748  cdleme42a  40841  cdleme42c  40842  cdlemg2fv2  40970  cdlemg2m  40974  cdlemg4g  40986  cdlemg4  40987  cdlemg6c  40990  cdlemg7aN  40995  cdlemg9a  41002  cdlemg9b  41003  cdlemg10c  41009  cdlemg12a  41013  cdlemg12b  41014  cdlemg17a  41031  cdlemg18b  41049  cdlemg18c  41050  trlcoabs2N  41092  trlcolem  41096  tendoco2  41138  tendoicl  41166  cdlemi1  41188  cdlemi2  41189  cdlemj3  41193  tendocan  41194  cdlemk3  41203  cdlemk4  41204  cdlemk5a  41205  cdlemk9  41209  cdlemk9bN  41210  cdlemk10  41213  cdlemk30  41264  cdlemk31  41266  cdlemk39  41286  cdlemkfid1N  41291  cdlemkfid2N  41293  cdlemk19ylem  41300  cdlemk19xlem  41312  cdlemk53b  41326  cdlemk53  41327  cdlemk55a  41329  cdlemk43N  41333  cdlemk19u1  41339  cdlemm10N  41488  cdlemn2  41565  cdlemn10  41576  dihjustlem  41586  dihord2cN  41591  dihvalcq2  41617  dihopelvalcpre  41618  dihord5b  41629  dihord6b  41630  dihmeetlem2N  41669  dihmeetbclemN  41674  dihmeetlem4preN  41676  dihmeetALTN  41697  dochshpncl  41754  dochsatshpb  41822  hdmapval3N  42208  hgmap11  42272  f1o2d2  42599  remulcand  42803  pellfundex  43237  congtr  43316  fzmaxdif  43332  isnumbasgrplem2  43455  idomsubgmo  43544  ntrclsk13  44421  grumnudlem  44635  restuni3  45471  unirnmapsn  45566  ssmapsn  45568  infnsuprnmpt  45602  upbdrech  45661  suplesup  45692  infleinf  45724  supxrunb3  45751  mullimc  45970  islptre  45973  mullimcf  45977  neglimc  45999  limsupmnfuzlem  46078  limsupre3lem  46084  limsupre3uzlem  46087  icccncfext  46239  dvmptfprod  46297  stoweidlem31  46383  opnvonmbllem2  46985  smflimsuplem7  47178  ormkglobd  47227  funressneu  47401  cfsetsnfsetf1  47413  prmdvdsfmtnof1lem1  47938  uhgrimisgrgriclem  48284  clnbgrgrim  48288  grlimedgclnbgr  48349  domnmsuppn0  48723  lincext3  48810  2arymaptfo  49008