Theorem simp1r 1217

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

Syntax hints:   → wi 4   ∧ wa 400   ∧ w3a 1103

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 210  df-an 401  df-3an 1105

This theorem is referenced by:  simp11r  1304  simp21r  1310  simp31r  1316  eqfunresadj  7360  offsplitfpar  8115  mpof1o2d  8122  poseq  8155  omeulem2  8569  uniinqs  8796  unxpdomlem3  9219  elfiun  9391  cofsmo  10254  isfin2-2  10304  isf32lem9  10346  tskun  10772  tskurn  10775  reclem3pr  11035  dedekind  11374  subaddmulsub  11678  dmdcan  11926  lt2msq1  12100  supmullem1  12186  supmul  12188  xaddass2  13277  xlt2add  13287  xmulasslem3  13313  iccsplit  13513  expaddzlem  14143  expaddz  14144  expmulz  14146  limsupgle  15530  o1add  15667  o1mul  15668  o1sub  15669  bitsfzo  16494  sadfval  16511  smufval  16536  nn0rppwr  16620  prmexpb  16779  4sqlem18  17023  vdwlem10  17051  setsstruct2  17235  mrieqv2d  17696  curf1  18282  chnccat  18683  mgmsscl  18704  mndpfsupp  18826  mndodcong  19613  subgabl  19907  gex2abl  19922  ogrpinvlt  20215  rng1zrlem  20260  cntzsubrng  20653  cntzsubr  20692  abvres  20915  lbsind2  21183  lbsextlem2  21264  lbsextg  21267  matring  22581  mdetunilem8  22757  maducoeval  22777  maducoeval2  22778  madurid  22782  cramerimplem3  22823  pmatcollpw2  22916  pm2mpf1  22937  cnprest  23427  isreg2  23515  fbssfi  23975  hausflimlem  24117  tmdgsum  24233  ssblps  24560  ssbl  24561  xrsmopn  24951  cphassi  25354  cphassir  25355  4cphipval2  25382  cphipval  25383  dvres2  26052  vieta1  26454  aalioulem4  26477  efgh  26684  cxpadd  26822  cxpsub  26825  divcxp  26830  cxple2  26840  cxplt2  26841  cxpcn3lem  26890  angcan  26945  ang180lem5  26956  isosctrlem3  26963  lgssq  27479  nosupinfsep  27874  noetalem1  27883  noeta2  27932  ltslpss  28079  bdayfinbndlem1  28638  brbtwn2  29233  axcontlem4  29295  axcontlem8  29299  uhgr2edg  29536  chscllem4  31970  cshwrnid  33259  pstmval  34263  measinblem  34588  cvmlift2lem6  35778  linethru  36623  cnres2  38392  lcv1  39793  lfl1  39822  lshpkrex  39870  hlrelat3  40164  cvrval3  40165  cvrval4N  40166  athgt  40208  atcvrlln2  40271  atcvrlln  40272  lvolnle3at  40334  lvolnlelpln  40337  4atlem11  40361  4atlem12  40364  2lplnj  40372  dalemddea  40436  cdlema2N  40544  paddasslem2  40573  atmod1i1m  40610  lhp2lt  40753  lhp0lt  40755  lhpexle3lem  40763  lhpj1  40774  lhpmcvr4N  40778  lhpelim  40789  lhpmod2i2  40790  lhpmod6i1  40791  cdlemb2  40793  lhpat  40795  ltrnatb  40889  ltrnel  40891  ltrncnvel  40894  ltrncnv  40898  trlval2  40915  trljat1  40918  trljat2  40919  trlnidatb  40929  cdlemc1  40943  cdlemc2  40944  cdlemc5  40947  cdlemc6  40948  cdleme0aa  40962  cdleme0b  40964  cdleme0c  40965  cdleme0e  40969  cdleme0fN  40970  cdleme01N  40973  cdleme0ex1N  40975  cdleme0moN  40977  cdleme3g  40986  cdleme3h  40987  cdleme3  40989  cdleme4  40990  cdleme4a  40991  cdleme5  40992  cdleme8  41002  cdleme9  41005  cdleme10  41006  cdleme16aN  41011  cdleme11fN  41016  cdleme11g  41017  cdleme11k  41020  cdleme13  41024  cdleme17c  41040  cdleme17d1  41041  cdleme18c  41045  cdleme22gb  41046  cdlemeda  41050  cdlemednpq  41051  cdlemednuN  41052  cdleme19c  41057  cdleme20aN  41061  cdleme20bN  41062  cdleme20c  41063  cdleme22aa  41091  cdleme22d  41095  cdleme22e  41096  cdleme27cl  41118  cdleme27a  41119  cdleme30a  41130  cdleme42a  41223  cdleme42c  41224  cdlemg2fv2  41352  cdlemg2m  41356  cdlemg4g  41368  cdlemg4  41369  cdlemg6c  41372  cdlemg7aN  41377  cdlemg9a  41384  cdlemg9b  41385  cdlemg10c  41391  cdlemg12a  41395  cdlemg12b  41396  cdlemg17a  41413  cdlemg18b  41431  cdlemg18c  41432  trlcoabs2N  41474  trlcolem  41478  tendoco2  41520  tendoicl  41548  cdlemi1  41570  cdlemi2  41571  cdlemj3  41575  tendocan  41576  cdlemk3  41585  cdlemk4  41586  cdlemk5a  41587  cdlemk9  41591  cdlemk9bN  41592  cdlemk10  41595  cdlemk30  41646  cdlemk31  41648  cdlemk39  41668  cdlemkfid1N  41673  cdlemkfid2N  41675  cdlemk19ylem  41682  cdlemk19xlem  41694  cdlemk53b  41708  cdlemk53  41709  cdlemk55a  41711  cdlemk43N  41715  cdlemk19u1  41721  cdlemm10N  41870  cdlemn2  41947  cdlemn10  41958  dihjustlem  41968  dihord2cN  41973  dihvalcq2  41999  dihopelvalcpre  42000  dihord5b  42011  dihord6b  42012  dihmeetlem2N  42051  dihmeetbclemN  42056  dihmeetlem4preN  42058  dihmeetALTN  42079  dochshpncl  42136  dochsatshpb  42204  hdmapval3N  42590  hgmap11  42654  remulcand  43178  pellfundex  43593  congtr  43672  fzmaxdif  43688  isnumbasgrplem2  43811  idomsubgmo  43900  ntrclsk13  44777  grumnudlem  44975  restuni3  45816  unirnmapsn  45910  ssmapsn  45912  infnsuprnmpt  45945  upbdrech  46004  suplesup  46035  infleinf  46067  supxrunb3  46094  mullimc  46312  islptre  46315  mullimcf  46319  neglimc  46341  limsupmnfuzlem  46420  limsupre3lem  46426  limsupre3uzlem  46429  icccncfext  46581  dvmptfprod  46639  stoweidlem31  46725  opnvonmbllem2  47327  smflimsuplem7  47520  ormkglobd  47571  funressneu  47761  cfsetsnfsetf1  47773  prmdvdsfmtnof1lem1  48313  uhgrimisgrgriclem  48672  clnbgrgrim  48676  grlimedgclnbgr  48737  domnmsuppn0  49126  lincext3  49213  2arymaptfo  49411