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

Syntax hints:   → wi 4   ∧ wa 397   ∧ w3a 1088

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 206  df-an 398  df-3an 1090

This theorem is referenced by:  simp11r  1286  simp21r  1292  simp31r  1298  eqfunresadj  7357  offsplitfpar  8105  poseq  8144  omeulem2  8583  uniinqs  8791  unxpdomlem3  9252  elfiun  9425  cofsmo  10264  isfin2-2  10314  isf32lem9  10356  tskun  10781  tskurn  10784  reclem3pr  11044  dedekind  11377  subaddmulsub  11677  dmdcan  11924  lt2msq1  12098  supmullem1  12184  supmul  12186  xaddass2  13229  xlt2add  13239  xmulasslem3  13265  iccsplit  13462  expaddzlem  14071  expaddz  14072  expmulz  14074  limsupgle  15421  o1add  15558  o1mul  15559  o1sub  15560  bitsfzo  16376  sadfval  16393  smufval  16418  prmexpb  16657  4sqlem18  16895  vdwlem10  16923  setsstruct2  17107  mrieqv2d  17583  curf1  18178  mgmsscl  18566  mndodcong  19410  subgabl  19704  gex2abl  19719  cntzsubr  20353  abvres  20447  lbsind2  20692  lbsextlem2  20772  lbsextg  20775  matring  21945  mdetunilem8  22121  maducoeval  22141  maducoeval2  22142  madurid  22146  cramerimplem3  22187  pmatcollpw2  22280  pm2mpf1  22301  cnprest  22793  isreg2  22881  fbssfi  23341  hausflimlem  23483  tmdgsum  23599  ssblps  23928  ssbl  23929  xrsmopn  24328  cphassi  24731  cphassir  24732  4cphipval2  24759  cphipval  24760  dvres2  25429  vieta1  25825  aalioulem4  25848  efgh  26050  cxpadd  26187  cxpsub  26190  divcxp  26195  cxple2  26205  cxplt2  26206  cxpcn3lem  26255  angcan  26307  ang180lem5  26318  isosctrlem3  26325  lgssq  26840  nosupinfsep  27235  noetalem1  27244  noeta2  27286  sltlpss  27401  brbtwn2  28163  axcontlem4  28225  axcontlem8  28229  uhgr2edg  28465  chscllem4  30893  cshwrnid  32125  ogrpinvlt  32241  pstmval  32875  measinblem  33218  cvmlift2lem6  34299  linethru  35125  cnres2  36631  lcv1  37911  lfl1  37940  lshpkrex  37988  hlrelat3  38283  cvrval3  38284  cvrval4N  38285  athgt  38327  atcvrlln2  38390  atcvrlln  38391  lvolnle3at  38453  lvolnlelpln  38456  4atlem11  38480  4atlem12  38483  2lplnj  38491  dalemddea  38555  cdlema2N  38663  paddasslem2  38692  atmod1i1m  38729  lhp2lt  38872  lhp0lt  38874  lhpexle3lem  38882  lhpj1  38893  lhpmcvr4N  38897  lhpelim  38908  lhpmod2i2  38909  lhpmod6i1  38910  cdlemb2  38912  lhpat  38914  ltrnatb  39008  ltrnel  39010  ltrncnvel  39013  ltrncnv  39017  trlval2  39034  trljat1  39037  trljat2  39038  trlnidatb  39048  cdlemc1  39062  cdlemc2  39063  cdlemc5  39066  cdlemc6  39067  cdleme0aa  39081  cdleme0b  39083  cdleme0c  39084  cdleme0e  39088  cdleme0fN  39089  cdleme01N  39092  cdleme0ex1N  39094  cdleme0moN  39096  cdleme3g  39105  cdleme3h  39106  cdleme3  39108  cdleme4  39109  cdleme4a  39110  cdleme5  39111  cdleme8  39121  cdleme9  39124  cdleme10  39125  cdleme16aN  39130  cdleme11fN  39135  cdleme11g  39136  cdleme11k  39139  cdleme13  39143  cdleme17c  39159  cdleme17d1  39160  cdleme18c  39164  cdleme22gb  39165  cdlemeda  39169  cdlemednpq  39170  cdlemednuN  39171  cdleme19c  39176  cdleme20aN  39180  cdleme20bN  39181  cdleme20c  39182  cdleme22aa  39210  cdleme22d  39214  cdleme22e  39215  cdleme27cl  39237  cdleme27a  39238  cdleme30a  39249  cdleme42a  39342  cdleme42c  39343  cdlemg2fv2  39471  cdlemg2m  39475  cdlemg4g  39487  cdlemg4  39488  cdlemg6c  39491  cdlemg7aN  39496  cdlemg9a  39503  cdlemg9b  39504  cdlemg10c  39510  cdlemg12a  39514  cdlemg12b  39515  cdlemg17a  39532  cdlemg18b  39550  cdlemg18c  39551  trlcoabs2N  39593  trlcolem  39597  tendoco2  39639  tendoicl  39667  cdlemi1  39689  cdlemi2  39690  cdlemj3  39694  tendocan  39695  cdlemk3  39704  cdlemk4  39705  cdlemk5a  39706  cdlemk9  39710  cdlemk9bN  39711  cdlemk10  39714  cdlemk30  39765  cdlemk31  39767  cdlemk39  39787  cdlemkfid1N  39792  cdlemkfid2N  39794  cdlemk19ylem  39801  cdlemk19xlem  39813  cdlemk53b  39827  cdlemk53  39828  cdlemk55a  39830  cdlemk43N  39834  cdlemk19u1  39840  cdlemm10N  39989  cdlemn2  40066  cdlemn10  40077  dihjustlem  40087  dihord2cN  40092  dihvalcq2  40118  dihopelvalcpre  40119  dihord5b  40130  dihord6b  40131  dihmeetlem2N  40170  dihmeetbclemN  40175  dihmeetlem4preN  40177  dihmeetALTN  40198  dochshpncl  40255  dochsatshpb  40323  hdmapval3N  40709  hgmap11  40773  f1o2d2  41055  nn0rppwr  41224  remulcand  41311  pellfundex  41624  congtr  41704  fzmaxdif  41720  isnumbasgrplem2  41846  idomsubgmo  41940  ntrclsk13  42822  grumnudlem  43044  restuni3  43807  unirnmapsn  43913  ssmapsn  43915  infnsuprnmpt  43954  upbdrech  44015  suplesup  44049  infleinf  44082  supxrunb3  44109  mullimc  44332  islptre  44335  mullimcf  44339  neglimc  44363  limsupmnfuzlem  44442  limsupre3lem  44448  limsupre3uzlem  44451  icccncfext  44603  dvmptfprod  44661  stoweidlem31  44747  opnvonmbllem2  45349  smflimsuplem7  45542  funressneu  45757  cfsetsnfsetf1  45769  prmdvdsfmtnof1lem1  46252  cntzsubrng  46746  domnmsuppn0  47045  mndpfsupp  47052  lincext3  47137  2arymaptfo  47340