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  7294  offsplitfpar  8049  poseq  8088  omeulem2  8498  uniinqs  8721  unxpdomlem3  9142  elfiun  9314  cofsmo  10157  isfin2-2  10207  isf32lem9  10249  tskun  10674  tskurn  10677  reclem3pr  10937  dedekind  11273  subaddmulsub  11577  dmdcan  11828  lt2msq1  12003  supmullem1  12089  supmul  12091  xaddass2  13146  xlt2add  13156  xmulasslem3  13182  iccsplit  13382  expaddzlem  14009  expaddz  14010  expmulz  14012  limsupgle  15381  o1add  15518  o1mul  15519  o1sub  15520  bitsfzo  16343  sadfval  16360  smufval  16385  nn0rppwr  16469  prmexpb  16627  4sqlem18  16871  vdwlem10  16899  setsstruct2  17082  mrieqv2d  17542  curf1  18128  chnccat  18529  mgmsscl  18550  mndpfsupp  18672  mndodcong  19452  subgabl  19746  gex2abl  19761  ogrpinvlt  20054  cntzsubrng  20480  cntzsubr  20519  abvres  20744  lbsind2  21013  lbsextlem2  21094  lbsextg  21097  matring  22356  mdetunilem8  22532  maducoeval  22552  maducoeval2  22553  madurid  22557  cramerimplem3  22598  pmatcollpw2  22691  pm2mpf1  22712  cnprest  23202  isreg2  23290  fbssfi  23750  hausflimlem  23892  tmdgsum  24008  ssblps  24335  ssbl  24336  xrsmopn  24726  cphassi  25139  cphassir  25140  4cphipval2  25167  cphipval  25168  dvres2  25838  vieta1  26245  aalioulem4  26268  efgh  26475  cxpadd  26613  cxpsub  26616  divcxp  26621  cxple2  26631  cxplt2  26632  cxpcn3lem  26682  angcan  26737  ang180lem5  26748  isosctrlem3  26755  lgssq  27273  nosupinfsep  27669  noetalem1  27678  noeta2  27722  sltlpss  27851  brbtwn2  28881  axcontlem4  28943  axcontlem8  28947  uhgr2edg  29184  chscllem4  31615  cshwrnid  32937  pstmval  33903  measinblem  34228  cvmlift2lem6  35340  linethru  36186  cnres2  37802  lcv1  39079  lfl1  39108  lshpkrex  39156  hlrelat3  39450  cvrval3  39451  cvrval4N  39452  athgt  39494  atcvrlln2  39557  atcvrlln  39558  lvolnle3at  39620  lvolnlelpln  39623  4atlem11  39647  4atlem12  39650  2lplnj  39658  dalemddea  39722  cdlema2N  39830  paddasslem2  39859  atmod1i1m  39896  lhp2lt  40039  lhp0lt  40041  lhpexle3lem  40049  lhpj1  40060  lhpmcvr4N  40064  lhpelim  40075  lhpmod2i2  40076  lhpmod6i1  40077  cdlemb2  40079  lhpat  40081  ltrnatb  40175  ltrnel  40177  ltrncnvel  40180  ltrncnv  40184  trlval2  40201  trljat1  40204  trljat2  40205  trlnidatb  40215  cdlemc1  40229  cdlemc2  40230  cdlemc5  40233  cdlemc6  40234  cdleme0aa  40248  cdleme0b  40250  cdleme0c  40251  cdleme0e  40255  cdleme0fN  40256  cdleme01N  40259  cdleme0ex1N  40261  cdleme0moN  40263  cdleme3g  40272  cdleme3h  40273  cdleme3  40275  cdleme4  40276  cdleme4a  40277  cdleme5  40278  cdleme8  40288  cdleme9  40291  cdleme10  40292  cdleme16aN  40297  cdleme11fN  40302  cdleme11g  40303  cdleme11k  40306  cdleme13  40310  cdleme17c  40326  cdleme17d1  40327  cdleme18c  40331  cdleme22gb  40332  cdlemeda  40336  cdlemednpq  40337  cdlemednuN  40338  cdleme19c  40343  cdleme20aN  40347  cdleme20bN  40348  cdleme20c  40349  cdleme22aa  40377  cdleme22d  40381  cdleme22e  40382  cdleme27cl  40404  cdleme27a  40405  cdleme30a  40416  cdleme42a  40509  cdleme42c  40510  cdlemg2fv2  40638  cdlemg2m  40642  cdlemg4g  40654  cdlemg4  40655  cdlemg6c  40658  cdlemg7aN  40663  cdlemg9a  40670  cdlemg9b  40671  cdlemg10c  40677  cdlemg12a  40681  cdlemg12b  40682  cdlemg17a  40699  cdlemg18b  40717  cdlemg18c  40718  trlcoabs2N  40760  trlcolem  40764  tendoco2  40806  tendoicl  40834  cdlemi1  40856  cdlemi2  40857  cdlemj3  40861  tendocan  40862  cdlemk3  40871  cdlemk4  40872  cdlemk5a  40873  cdlemk9  40877  cdlemk9bN  40878  cdlemk10  40881  cdlemk30  40932  cdlemk31  40934  cdlemk39  40954  cdlemkfid1N  40959  cdlemkfid2N  40961  cdlemk19ylem  40968  cdlemk19xlem  40980  cdlemk53b  40994  cdlemk53  40995  cdlemk55a  40997  cdlemk43N  41001  cdlemk19u1  41007  cdlemm10N  41156  cdlemn2  41233  cdlemn10  41244  dihjustlem  41254  dihord2cN  41259  dihvalcq2  41285  dihopelvalcpre  41286  dihord5b  41297  dihord6b  41298  dihmeetlem2N  41337  dihmeetbclemN  41342  dihmeetlem4preN  41344  dihmeetALTN  41365  dochshpncl  41422  dochsatshpb  41490  hdmapval3N  41876  hgmap11  41940  f1o2d2  42265  remulcand  42471  pellfundex  42918  congtr  42997  fzmaxdif  43013  isnumbasgrplem2  43136  idomsubgmo  43225  ntrclsk13  44103  grumnudlem  44317  restuni3  45154  unirnmapsn  45250  ssmapsn  45252  infnsuprnmpt  45286  upbdrech  45345  suplesup  45377  infleinf  45409  supxrunb3  45436  mullimc  45655  islptre  45658  mullimcf  45662  neglimc  45684  limsupmnfuzlem  45763  limsupre3lem  45769  limsupre3uzlem  45772  icccncfext  45924  dvmptfprod  45982  stoweidlem31  46068  opnvonmbllem2  46670  smflimsuplem7  46863  ormkglobd  46912  funressneu  47077  cfsetsnfsetf1  47089  prmdvdsfmtnof1lem1  47614  uhgrimisgrgriclem  47960  clnbgrgrim  47964  grlimedgclnbgr  48025  domnmsuppn0  48399  lincext3  48487  2arymaptfo  48685