Theorem simp1r 1211

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 488	. 2 ⊢ ((𝜑 ∧ 𝜓) → 𝜓)
2	1	3ad2ant1 1145	1 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒 ∧ 𝜃) → 𝜓)

Syntax hints:   → wi 4   ∧ wa 399   ∧ w3a 1097

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 209  df-an 400  df-3an 1099

This theorem is referenced by:  simp11r  1298  simp21r  1304  simp31r  1310  eqfunresadj  7340  offsplitfpar  8093  mpof1o2d  8100  poseq  8133  omeulem2  8547  uniinqs  8774  unxpdomlem3  9198  elfiun  9373  cofsmo  10223  isfin2-2  10273  isf32lem9  10315  tskun  10741  tskurn  10744  reclem3pr  11004  dedekind  11343  subaddmulsub  11647  dmdcan  11898  lt2msq1  12073  supmullem1  12159  supmul  12161  xaddass2  13250  xlt2add  13260  xmulasslem3  13286  iccsplit  13486  expaddzlem  14115  expaddz  14116  expmulz  14118  limsupgle  15487  o1add  15624  o1mul  15625  o1sub  15626  bitsfzo  16452  sadfval  16469  smufval  16494  nn0rppwr  16578  prmexpb  16737  4sqlem18  16981  vdwlem10  17009  setsstruct2  17193  mrieqv2d  17654  curf1  18240  chnccat  18641  mgmsscl  18662  mndpfsupp  18784  mndodcong  19565  subgabl  19859  gex2abl  19874  ogrpinvlt  20167  cntzsubrng  20596  cntzsubr  20635  abvres  20860  lbsind2  21128  lbsextlem2  21209  lbsextg  21212  matring  22483  mdetunilem8  22659  maducoeval  22679  maducoeval2  22680  madurid  22684  cramerimplem3  22725  pmatcollpw2  22818  pm2mpf1  22839  cnprest  23329  isreg2  23417  fbssfi  23877  hausflimlem  24019  tmdgsum  24135  ssblps  24462  ssbl  24463  xrsmopn  24853  cphassi  25256  cphassir  25257  4cphipval2  25284  cphipval  25285  dvres2  25954  vieta1  26353  aalioulem4  26376  efgh  26583  cxpadd  26721  cxpsub  26724  divcxp  26729  cxple2  26739  cxplt2  26740  cxpcn3lem  26789  angcan  26844  ang180lem5  26855  isosctrlem3  26862  lgssq  27378  nosupinfsep  27773  noetalem1  27782  noeta2  27831  ltslpss  27978  bdayfinbndlem1  28537  brbtwn2  29052  axcontlem4  29114  axcontlem8  29118  uhgr2edg  29355  chscllem4  31789  cshwrnid  33100  pstmval  34153  measinblem  34478  cvmlift2lem6  35622  linethru  36467  cnres2  38226  lcv1  39629  lfl1  39658  lshpkrex  39706  hlrelat3  40000  cvrval3  40001  cvrval4N  40002  athgt  40044  atcvrlln2  40107  atcvrlln  40108  lvolnle3at  40170  lvolnlelpln  40173  4atlem11  40197  4atlem12  40200  2lplnj  40208  dalemddea  40272  cdlema2N  40380  paddasslem2  40409  atmod1i1m  40446  lhp2lt  40589  lhp0lt  40591  lhpexle3lem  40599  lhpj1  40610  lhpmcvr4N  40614  lhpelim  40625  lhpmod2i2  40626  lhpmod6i1  40627  cdlemb2  40629  lhpat  40631  ltrnatb  40725  ltrnel  40727  ltrncnvel  40730  ltrncnv  40734  trlval2  40751  trljat1  40754  trljat2  40755  trlnidatb  40765  cdlemc1  40779  cdlemc2  40780  cdlemc5  40783  cdlemc6  40784  cdleme0aa  40798  cdleme0b  40800  cdleme0c  40801  cdleme0e  40805  cdleme0fN  40806  cdleme01N  40809  cdleme0ex1N  40811  cdleme0moN  40813  cdleme3g  40822  cdleme3h  40823  cdleme3  40825  cdleme4  40826  cdleme4a  40827  cdleme5  40828  cdleme8  40838  cdleme9  40841  cdleme10  40842  cdleme16aN  40847  cdleme11fN  40852  cdleme11g  40853  cdleme11k  40856  cdleme13  40860  cdleme17c  40876  cdleme17d1  40877  cdleme18c  40881  cdleme22gb  40882  cdlemeda  40886  cdlemednpq  40887  cdlemednuN  40888  cdleme19c  40893  cdleme20aN  40897  cdleme20bN  40898  cdleme20c  40899  cdleme22aa  40927  cdleme22d  40931  cdleme22e  40932  cdleme27cl  40954  cdleme27a  40955  cdleme30a  40966  cdleme42a  41059  cdleme42c  41060  cdlemg2fv2  41188  cdlemg2m  41192  cdlemg4g  41204  cdlemg4  41205  cdlemg6c  41208  cdlemg7aN  41213  cdlemg9a  41220  cdlemg9b  41221  cdlemg10c  41227  cdlemg12a  41231  cdlemg12b  41232  cdlemg17a  41249  cdlemg18b  41267  cdlemg18c  41268  trlcoabs2N  41310  trlcolem  41314  tendoco2  41356  tendoicl  41384  cdlemi1  41406  cdlemi2  41407  cdlemj3  41411  tendocan  41412  cdlemk3  41421  cdlemk4  41422  cdlemk5a  41423  cdlemk9  41427  cdlemk9bN  41428  cdlemk10  41431  cdlemk30  41482  cdlemk31  41484  cdlemk39  41504  cdlemkfid1N  41509  cdlemkfid2N  41511  cdlemk19ylem  41518  cdlemk19xlem  41530  cdlemk53b  41544  cdlemk53  41545  cdlemk55a  41547  cdlemk43N  41551  cdlemk19u1  41557  cdlemm10N  41706  cdlemn2  41783  cdlemn10  41794  dihjustlem  41804  dihord2cN  41809  dihvalcq2  41835  dihopelvalcpre  41836  dihord5b  41847  dihord6b  41848  dihmeetlem2N  41887  dihmeetbclemN  41892  dihmeetlem4preN  41894  dihmeetALTN  41915  dochshpncl  41972  dochsatshpb  42040  hdmapval3N  42426  hgmap11  42490  remulcand  43012  pellfundex  43427  congtr  43506  fzmaxdif  43522  isnumbasgrplem2  43645  idomsubgmo  43734  ntrclsk13  44611  grumnudlem  44825  restuni3  45660  unirnmapsn  45754  ssmapsn  45756  infnsuprnmpt  45789  upbdrech  45848  suplesup  45879  infleinf  45911  supxrunb3  45938  mullimc  46156  islptre  46159  mullimcf  46163  neglimc  46185  limsupmnfuzlem  46264  limsupre3lem  46270  limsupre3uzlem  46273  icccncfext  46425  dvmptfprod  46483  stoweidlem31  46569  opnvonmbllem2  47171  smflimsuplem7  47364  ormkglobd  47415  funressneu  47605  cfsetsnfsetf1  47617  prmdvdsfmtnof1lem1  48157  uhgrimisgrgriclem  48516  clnbgrgrim  48520  grlimedgclnbgr  48581  domnmsuppn0  48955  lincext3  49042  2arymaptfo  49240