Theorem simp1r 1198

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

Syntax hints:   → wi 4   ∧ wa 396   ∧ w3a 1087

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 397  df-3an 1089

This theorem is referenced by:  simp11r  1285  simp21r  1291  simp31r  1297  eqfunresadj  7310  offsplitfpar  8056  poseq  8095  omeulem2  8535  uniinqs  8743  unxpdomlem3  9203  elfiun  9375  cofsmo  10214  isfin2-2  10264  isf32lem9  10306  tskun  10731  tskurn  10734  reclem3pr  10994  dedekind  11327  subaddmulsub  11627  dmdcan  11874  lt2msq1  12048  supmullem1  12134  supmul  12136  xaddass2  13179  xlt2add  13189  xmulasslem3  13215  iccsplit  13412  expaddzlem  14021  expaddz  14022  expmulz  14024  limsupgle  15371  o1add  15508  o1mul  15509  o1sub  15510  bitsfzo  16326  sadfval  16343  smufval  16368  prmexpb  16607  4sqlem18  16845  vdwlem10  16873  setsstruct2  17057  mrieqv2d  17533  curf1  18128  mgmsscl  18516  mndodcong  19338  subgabl  19628  gex2abl  19643  cntzsubr  20305  abvres  20354  lbsind2  20599  lbsextlem2  20679  lbsextg  20682  matring  21829  mdetunilem8  22005  maducoeval  22025  maducoeval2  22026  madurid  22030  cramerimplem3  22071  pmatcollpw2  22164  pm2mpf1  22185  cnprest  22677  isreg2  22765  fbssfi  23225  hausflimlem  23367  tmdgsum  23483  ssblps  23812  ssbl  23813  xrsmopn  24212  cphassi  24615  cphassir  24616  4cphipval2  24643  cphipval  24644  dvres2  25313  vieta1  25709  aalioulem4  25732  efgh  25934  cxpadd  26071  cxpsub  26074  divcxp  26079  cxple2  26089  cxplt2  26090  cxpcn3lem  26137  angcan  26189  ang180lem5  26200  isosctrlem3  26207  lgssq  26722  nosupinfsep  27117  noetalem1  27126  noeta2  27167  sltlpss  27279  brbtwn2  27917  axcontlem4  27979  axcontlem8  27983  uhgr2edg  28219  chscllem4  30645  cshwrnid  31885  ogrpinvlt  32001  pstmval  32565  measinblem  32908  cvmlift2lem6  33989  linethru  34814  cnres2  36295  lcv1  37576  lfl1  37605  lshpkrex  37653  hlrelat3  37948  cvrval3  37949  cvrval4N  37950  athgt  37992  atcvrlln2  38055  atcvrlln  38056  lvolnle3at  38118  lvolnlelpln  38121  4atlem11  38145  4atlem12  38148  2lplnj  38156  dalemddea  38220  cdlema2N  38328  paddasslem2  38357  atmod1i1m  38394  lhp2lt  38537  lhp0lt  38539  lhpexle3lem  38547  lhpj1  38558  lhpmcvr4N  38562  lhpelim  38573  lhpmod2i2  38574  lhpmod6i1  38575  cdlemb2  38577  lhpat  38579  ltrnatb  38673  ltrnel  38675  ltrncnvel  38678  ltrncnv  38682  trlval2  38699  trljat1  38702  trljat2  38703  trlnidatb  38713  cdlemc1  38727  cdlemc2  38728  cdlemc5  38731  cdlemc6  38732  cdleme0aa  38746  cdleme0b  38748  cdleme0c  38749  cdleme0e  38753  cdleme0fN  38754  cdleme01N  38757  cdleme0ex1N  38759  cdleme0moN  38761  cdleme3g  38770  cdleme3h  38771  cdleme3  38773  cdleme4  38774  cdleme4a  38775  cdleme5  38776  cdleme8  38786  cdleme9  38789  cdleme10  38790  cdleme16aN  38795  cdleme11fN  38800  cdleme11g  38801  cdleme11k  38804  cdleme13  38808  cdleme17c  38824  cdleme17d1  38825  cdleme18c  38829  cdleme22gb  38830  cdlemeda  38834  cdlemednpq  38835  cdlemednuN  38836  cdleme19c  38841  cdleme20aN  38845  cdleme20bN  38846  cdleme20c  38847  cdleme22aa  38875  cdleme22d  38879  cdleme22e  38880  cdleme27cl  38902  cdleme27a  38903  cdleme30a  38914  cdleme42a  39007  cdleme42c  39008  cdlemg2fv2  39136  cdlemg2m  39140  cdlemg4g  39152  cdlemg4  39153  cdlemg6c  39156  cdlemg7aN  39161  cdlemg9a  39168  cdlemg9b  39169  cdlemg10c  39175  cdlemg12a  39179  cdlemg12b  39180  cdlemg17a  39197  cdlemg18b  39215  cdlemg18c  39216  trlcoabs2N  39258  trlcolem  39262  tendoco2  39304  tendoicl  39332  cdlemi1  39354  cdlemi2  39355  cdlemj3  39359  tendocan  39360  cdlemk3  39369  cdlemk4  39370  cdlemk5a  39371  cdlemk9  39375  cdlemk9bN  39376  cdlemk10  39379  cdlemk30  39430  cdlemk31  39432  cdlemk39  39452  cdlemkfid1N  39457  cdlemkfid2N  39459  cdlemk19ylem  39466  cdlemk19xlem  39478  cdlemk53b  39492  cdlemk53  39493  cdlemk55a  39495  cdlemk43N  39499  cdlemk19u1  39505  cdlemm10N  39654  cdlemn2  39731  cdlemn10  39742  dihjustlem  39752  dihord2cN  39757  dihvalcq2  39783  dihopelvalcpre  39784  dihord5b  39795  dihord6b  39796  dihmeetlem2N  39835  dihmeetbclemN  39840  dihmeetlem4preN  39842  dihmeetALTN  39863  dochshpncl  39920  dochsatshpb  39988  hdmapval3N  40374  hgmap11  40438  nn0rppwr  40877  remulcand  40965  pellfundex  41267  congtr  41347  fzmaxdif  41363  isnumbasgrplem2  41489  idomsubgmo  41583  ntrclsk13  42465  grumnudlem  42687  restuni3  43450  unirnmapsn  43556  ssmapsn  43558  infnsuprnmpt  43599  upbdrech  43660  suplesup  43694  infleinf  43727  supxrunb3  43754  mullimc  43977  islptre  43980  mullimcf  43984  neglimc  44008  limsupmnfuzlem  44087  limsupre3lem  44093  limsupre3uzlem  44096  icccncfext  44248  dvmptfprod  44306  stoweidlem31  44392  opnvonmbllem2  44994  smflimsuplem7  45187  funressneu  45401  cfsetsnfsetf1  45413  prmdvdsfmtnof1lem1  45896  domnmsuppn0  46565  mndpfsupp  46572  lincext3  46657  2arymaptfo  46860