Theorem simp1r 1197

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 1132	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  1284  simp21r  1290  simp31r  1296  eqfunresadj  7379  offsplitfpar  8142  poseq  8181  omeulem2  8619  uniinqs  8835  unxpdomlem3  9285  elfiun  9467  cofsmo  10306  isfin2-2  10356  isf32lem9  10398  tskun  10823  tskurn  10826  reclem3pr  11086  dedekind  11421  subaddmulsub  11723  dmdcan  11974  lt2msq1  12149  supmullem1  12235  supmul  12237  xaddass2  13288  xlt2add  13298  xmulasslem3  13324  iccsplit  13521  expaddzlem  14142  expaddz  14143  expmulz  14145  limsupgle  15509  o1add  15646  o1mul  15647  o1sub  15648  bitsfzo  16468  sadfval  16485  smufval  16510  nn0rppwr  16594  prmexpb  16752  4sqlem18  16995  vdwlem10  17023  setsstruct2  17207  mrieqv2d  17683  curf1  18281  mgmsscl  18670  mndpfsupp  18792  mndodcong  19574  subgabl  19868  gex2abl  19883  cntzsubrng  20583  cntzsubr  20622  abvres  20848  lbsind2  21097  lbsextlem2  21178  lbsextg  21181  matring  22464  mdetunilem8  22640  maducoeval  22660  maducoeval2  22661  madurid  22665  cramerimplem3  22706  pmatcollpw2  22799  pm2mpf1  22820  cnprest  23312  isreg2  23400  fbssfi  23860  hausflimlem  24002  tmdgsum  24118  ssblps  24447  ssbl  24448  xrsmopn  24847  cphassi  25261  cphassir  25262  4cphipval2  25289  cphipval  25290  dvres2  25961  vieta1  26368  aalioulem4  26391  efgh  26597  cxpadd  26735  cxpsub  26738  divcxp  26743  cxple2  26753  cxplt2  26754  cxpcn3lem  26804  angcan  26859  ang180lem5  26870  isosctrlem3  26877  lgssq  27395  nosupinfsep  27791  noetalem1  27800  noeta2  27843  sltlpss  27959  brbtwn2  28934  axcontlem4  28996  axcontlem8  29000  uhgr2edg  29239  chscllem4  31668  cshwrnid  32930  ogrpinvlt  33082  pstmval  33855  measinblem  34200  cvmlift2lem6  35292  linethru  36134  cnres2  37749  lcv1  39022  lfl1  39051  lshpkrex  39099  hlrelat3  39394  cvrval3  39395  cvrval4N  39396  athgt  39438  atcvrlln2  39501  atcvrlln  39502  lvolnle3at  39564  lvolnlelpln  39567  4atlem11  39591  4atlem12  39594  2lplnj  39602  dalemddea  39666  cdlema2N  39774  paddasslem2  39803  atmod1i1m  39840  lhp2lt  39983  lhp0lt  39985  lhpexle3lem  39993  lhpj1  40004  lhpmcvr4N  40008  lhpelim  40019  lhpmod2i2  40020  lhpmod6i1  40021  cdlemb2  40023  lhpat  40025  ltrnatb  40119  ltrnel  40121  ltrncnvel  40124  ltrncnv  40128  trlval2  40145  trljat1  40148  trljat2  40149  trlnidatb  40159  cdlemc1  40173  cdlemc2  40174  cdlemc5  40177  cdlemc6  40178  cdleme0aa  40192  cdleme0b  40194  cdleme0c  40195  cdleme0e  40199  cdleme0fN  40200  cdleme01N  40203  cdleme0ex1N  40205  cdleme0moN  40207  cdleme3g  40216  cdleme3h  40217  cdleme3  40219  cdleme4  40220  cdleme4a  40221  cdleme5  40222  cdleme8  40232  cdleme9  40235  cdleme10  40236  cdleme16aN  40241  cdleme11fN  40246  cdleme11g  40247  cdleme11k  40250  cdleme13  40254  cdleme17c  40270  cdleme17d1  40271  cdleme18c  40275  cdleme22gb  40276  cdlemeda  40280  cdlemednpq  40281  cdlemednuN  40282  cdleme19c  40287  cdleme20aN  40291  cdleme20bN  40292  cdleme20c  40293  cdleme22aa  40321  cdleme22d  40325  cdleme22e  40326  cdleme27cl  40348  cdleme27a  40349  cdleme30a  40360  cdleme42a  40453  cdleme42c  40454  cdlemg2fv2  40582  cdlemg2m  40586  cdlemg4g  40598  cdlemg4  40599  cdlemg6c  40602  cdlemg7aN  40607  cdlemg9a  40614  cdlemg9b  40615  cdlemg10c  40621  cdlemg12a  40625  cdlemg12b  40626  cdlemg17a  40643  cdlemg18b  40661  cdlemg18c  40662  trlcoabs2N  40704  trlcolem  40708  tendoco2  40750  tendoicl  40778  cdlemi1  40800  cdlemi2  40801  cdlemj3  40805  tendocan  40806  cdlemk3  40815  cdlemk4  40816  cdlemk5a  40817  cdlemk9  40821  cdlemk9bN  40822  cdlemk10  40825  cdlemk30  40876  cdlemk31  40878  cdlemk39  40898  cdlemkfid1N  40903  cdlemkfid2N  40905  cdlemk19ylem  40912  cdlemk19xlem  40924  cdlemk53b  40938  cdlemk53  40939  cdlemk55a  40941  cdlemk43N  40945  cdlemk19u1  40951  cdlemm10N  41100  cdlemn2  41177  cdlemn10  41188  dihjustlem  41198  dihord2cN  41203  dihvalcq2  41229  dihopelvalcpre  41230  dihord5b  41241  dihord6b  41242  dihmeetlem2N  41281  dihmeetbclemN  41286  dihmeetlem4preN  41288  dihmeetALTN  41309  dochshpncl  41366  dochsatshpb  41434  hdmapval3N  41820  hgmap11  41884  f1o2d2  42252  remulcand  42444  pellfundex  42873  congtr  42953  fzmaxdif  42969  isnumbasgrplem2  43092  idomsubgmo  43181  ntrclsk13  44060  grumnudlem  44280  restuni3  45057  unirnmapsn  45156  ssmapsn  45158  infnsuprnmpt  45194  upbdrech  45255  suplesup  45288  infleinf  45321  supxrunb3  45348  mullimc  45571  islptre  45574  mullimcf  45578  neglimc  45602  limsupmnfuzlem  45681  limsupre3lem  45687  limsupre3uzlem  45690  icccncfext  45842  dvmptfprod  45900  stoweidlem31  45986  opnvonmbllem2  46588  smflimsuplem7  46781  funressneu  46996  cfsetsnfsetf1  47008  prmdvdsfmtnof1lem1  47508  uhgrimisgrgriclem  47835  clnbgrgrim  47839  domnmsuppn0  48213  lincext3  48301  2arymaptfo  48503