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  7300  offsplitfpar  8055  poseq  8094  omeulem2  8504  uniinqs  8727  unxpdomlem3  9149  elfiun  9321  cofsmo  10167  isfin2-2  10217  isf32lem9  10259  tskun  10684  tskurn  10687  reclem3pr  10947  dedekind  11283  subaddmulsub  11587  dmdcan  11838  lt2msq1  12013  supmullem1  12099  supmul  12101  xaddass2  13151  xlt2add  13161  xmulasslem3  13187  iccsplit  13387  expaddzlem  14014  expaddz  14015  expmulz  14017  limsupgle  15386  o1add  15523  o1mul  15524  o1sub  15525  bitsfzo  16348  sadfval  16365  smufval  16390  nn0rppwr  16474  prmexpb  16632  4sqlem18  16876  vdwlem10  16904  setsstruct2  17087  mrieqv2d  17547  curf1  18133  chnccat  18534  mgmsscl  18555  mndpfsupp  18677  mndodcong  19456  subgabl  19750  gex2abl  19765  ogrpinvlt  20058  cntzsubrng  20484  cntzsubr  20523  abvres  20748  lbsind2  21017  lbsextlem2  21098  lbsextg  21101  matring  22359  mdetunilem8  22535  maducoeval  22555  maducoeval2  22556  madurid  22560  cramerimplem3  22601  pmatcollpw2  22694  pm2mpf1  22715  cnprest  23205  isreg2  23293  fbssfi  23753  hausflimlem  23895  tmdgsum  24011  ssblps  24338  ssbl  24339  xrsmopn  24729  cphassi  25142  cphassir  25143  4cphipval2  25170  cphipval  25171  dvres2  25841  vieta1  26248  aalioulem4  26271  efgh  26478  cxpadd  26616  cxpsub  26619  divcxp  26624  cxple2  26634  cxplt2  26635  cxpcn3lem  26685  angcan  26740  ang180lem5  26751  isosctrlem3  26758  lgssq  27276  nosupinfsep  27672  noetalem1  27681  noeta2  27725  sltlpss  27854  brbtwn2  28885  axcontlem4  28947  axcontlem8  28951  uhgr2edg  29188  chscllem4  31622  cshwrnid  32949  pstmval  33929  measinblem  34254  cvmlift2lem6  35373  linethru  36218  cnres2  37824  lcv1  39161  lfl1  39190  lshpkrex  39238  hlrelat3  39532  cvrval3  39533  cvrval4N  39534  athgt  39576  atcvrlln2  39639  atcvrlln  39640  lvolnle3at  39702  lvolnlelpln  39705  4atlem11  39729  4atlem12  39732  2lplnj  39740  dalemddea  39804  cdlema2N  39912  paddasslem2  39941  atmod1i1m  39978  lhp2lt  40121  lhp0lt  40123  lhpexle3lem  40131  lhpj1  40142  lhpmcvr4N  40146  lhpelim  40157  lhpmod2i2  40158  lhpmod6i1  40159  cdlemb2  40161  lhpat  40163  ltrnatb  40257  ltrnel  40259  ltrncnvel  40262  ltrncnv  40266  trlval2  40283  trljat1  40286  trljat2  40287  trlnidatb  40297  cdlemc1  40311  cdlemc2  40312  cdlemc5  40315  cdlemc6  40316  cdleme0aa  40330  cdleme0b  40332  cdleme0c  40333  cdleme0e  40337  cdleme0fN  40338  cdleme01N  40341  cdleme0ex1N  40343  cdleme0moN  40345  cdleme3g  40354  cdleme3h  40355  cdleme3  40357  cdleme4  40358  cdleme4a  40359  cdleme5  40360  cdleme8  40370  cdleme9  40373  cdleme10  40374  cdleme16aN  40379  cdleme11fN  40384  cdleme11g  40385  cdleme11k  40388  cdleme13  40392  cdleme17c  40408  cdleme17d1  40409  cdleme18c  40413  cdleme22gb  40414  cdlemeda  40418  cdlemednpq  40419  cdlemednuN  40420  cdleme19c  40425  cdleme20aN  40429  cdleme20bN  40430  cdleme20c  40431  cdleme22aa  40459  cdleme22d  40463  cdleme22e  40464  cdleme27cl  40486  cdleme27a  40487  cdleme30a  40498  cdleme42a  40591  cdleme42c  40592  cdlemg2fv2  40720  cdlemg2m  40724  cdlemg4g  40736  cdlemg4  40737  cdlemg6c  40740  cdlemg7aN  40745  cdlemg9a  40752  cdlemg9b  40753  cdlemg10c  40759  cdlemg12a  40763  cdlemg12b  40764  cdlemg17a  40781  cdlemg18b  40799  cdlemg18c  40800  trlcoabs2N  40842  trlcolem  40846  tendoco2  40888  tendoicl  40916  cdlemi1  40938  cdlemi2  40939  cdlemj3  40943  tendocan  40944  cdlemk3  40953  cdlemk4  40954  cdlemk5a  40955  cdlemk9  40959  cdlemk9bN  40960  cdlemk10  40963  cdlemk30  41014  cdlemk31  41016  cdlemk39  41036  cdlemkfid1N  41041  cdlemkfid2N  41043  cdlemk19ylem  41050  cdlemk19xlem  41062  cdlemk53b  41076  cdlemk53  41077  cdlemk55a  41079  cdlemk43N  41083  cdlemk19u1  41089  cdlemm10N  41238  cdlemn2  41315  cdlemn10  41326  dihjustlem  41336  dihord2cN  41341  dihvalcq2  41367  dihopelvalcpre  41368  dihord5b  41379  dihord6b  41380  dihmeetlem2N  41419  dihmeetbclemN  41424  dihmeetlem4preN  41426  dihmeetALTN  41447  dochshpncl  41504  dochsatshpb  41572  hdmapval3N  41958  hgmap11  42022  f1o2d2  42352  remulcand  42558  pellfundex  43004  congtr  43083  fzmaxdif  43099  isnumbasgrplem2  43222  idomsubgmo  43311  ntrclsk13  44189  grumnudlem  44403  restuni3  45240  unirnmapsn  45336  ssmapsn  45338  infnsuprnmpt  45372  upbdrech  45431  suplesup  45463  infleinf  45495  supxrunb3  45522  mullimc  45741  islptre  45744  mullimcf  45748  neglimc  45770  limsupmnfuzlem  45849  limsupre3lem  45855  limsupre3uzlem  45858  icccncfext  46010  dvmptfprod  46068  stoweidlem31  46154  opnvonmbllem2  46756  smflimsuplem7  46949  ormkglobd  46998  funressneu  47172  cfsetsnfsetf1  47184  prmdvdsfmtnof1lem1  47709  uhgrimisgrgriclem  48055  clnbgrgrim  48059  grlimedgclnbgr  48120  domnmsuppn0  48494  lincext3  48582  2arymaptfo  48780