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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∧ w3a 1103

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105

This theorem is used by:  simp11r  1304  simp21r  1310  simp31r  1316  eqfunresadj  7362  offsplitfpar  8119  mpof1o2d  8126  poseq  8159  omeulem2  8575  uniinqs  8802  unxpdomlem3  9233  elfiun  9406  cofsmo  10328  isfin2-2  10378  isf32lem9  10420  tskun  10852  tskurn  10855  reclem3pr  11115  dedekind  11454  subaddmulsub  11760  dmdcan  12008  lt2msq1  12182  supmullem1  12268  supmul  12270  xaddass2  13361  xlt2add  13371  xmulasslem3  13397  iccsplit  13597  expaddzlem  14228  expaddz  14229  expmulz  14231  limsupgle  15624  o1add  15761  o1mul  15762  o1sub  15763  bitsfzo  16585  sadfval  16602  smufval  16627  nn0rppwr  16715  prmexpb  16875  4sqlem18  17120  vdwlem10  17148  setsstruct2  17332  mrieqv2d  17793  curf1  18379  chnccat  18780  mgmsscl  18801  mndpfsupp  18941  mndodcong  19736  subgabl  20030  gex2abl  20045  ogrpinvlt  20338  rng1zrlem  20383  cntzsubrng  20799  cntzsubr  20838  abvres  21068  lbsind2  21336  lbsextlem2  21417  lbsextg  21420  matring  22738  mdetunilem8  22914  maducoeval  22934  maducoeval2  22935  madurid  22939  cramerimplem3  22983  pmatcollpw2  23076  pm2mpf1  23097  cnprest  23587  isreg2  23675  fbssfi  24136  hausflimlem  24278  tmdgsum  24394  ssblps  24721  ssbl  24722  xrsmopn  25112  cphassi  25515  cphassir  25516  4cphipval2  25543  cphipval  25544  dvres2  26212  vieta1  26617  aalioulem4  26644  efgh  26851  cxpadd  26989  cxpsub  26992  divcxp  26997  cxple2  27007  cxplt2  27008  cxpcn3lem  27057  angcan  27112  ang180lem5  27123  isosctrlem3  27130  lgssq  27646  nosupinfsep  28071  noetalem1  28080  noeta2  28129  ltslpss  28276  bdayfinbndlem1  28835  brbtwn2  29465  axcontlem4  29527  axcontlem8  29531  uhgr2edg  29771  chscllem4  32224  cshwrnid  33504  pstmval  34509  measinblem  34835  cvmlift2lem6  36042  linethru  36888  cnres2  38665  lcv1  40066  lfl1  40095  lshpkrex  40143  hlrelat3  40437  cvrval3  40438  cvrval4N  40439  athgt  40481  atcvrlln2  40544  atcvrlln  40545  lvolnle3at  40607  lvolnlelpln  40610  4atlem11  40634  4atlem12  40637  2lplnj  40645  dalemddea  40709  cdlema2N  40817  paddasslem2  40846  atmod1i1m  40883  lhp2lt  41026  lhp0lt  41028  lhpexle3lem  41036  lhpj1  41047  lhpmcvr4N  41051  lhpelim  41062  lhpmod2i2  41063  lhpmod6i1  41064  cdlemb2  41066  lhpat  41068  ltrnatb  41162  ltrnel  41164  ltrncnvel  41167  ltrncnv  41171  trlval2  41188  trljat1  41191  trljat2  41192  trlnidatb  41202  cdlemc1  41216  cdlemc2  41217  cdlemc5  41220  cdlemc6  41221  cdleme0aa  41235  cdleme0b  41237  cdleme0c  41238  cdleme0e  41242  cdleme0fN  41243  cdleme01N  41246  cdleme0ex1N  41248  cdleme0moN  41250  cdleme3g  41259  cdleme3h  41260  cdleme3  41262  cdleme4  41263  cdleme4a  41264  cdleme5  41265  cdleme8  41275  cdleme9  41278  cdleme10  41279  cdleme16aN  41284  cdleme11fN  41289  cdleme11g  41290  cdleme11k  41293  cdleme13  41297  cdleme17c  41313  cdleme17d1  41314  cdleme18c  41318  cdleme22gb  41319  cdlemeda  41323  cdlemednpq  41324  cdlemednuN  41325  cdleme19c  41330  cdleme20aN  41334  cdleme20bN  41335  cdleme20c  41336  cdleme22aa  41364  cdleme22d  41368  cdleme22e  41369  cdleme27cl  41391  cdleme27a  41392  cdleme30a  41403  cdleme42a  41496  cdleme42c  41497  cdlemg2fv2  41625  cdlemg2m  41629  cdlemg4g  41641  cdlemg4  41642  cdlemg6c  41645  cdlemg7aN  41650  cdlemg9a  41657  cdlemg9b  41658  cdlemg10c  41664  cdlemg12a  41668  cdlemg12b  41669  cdlemg17a  41686  cdlemg18b  41704  cdlemg18c  41705  trlcoabs2N  41747  trlcolem  41751  tendoco2  41793  tendoicl  41821  cdlemi1  41843  cdlemi2  41844  cdlemj3  41848  tendocan  41849  cdlemk3  41858  cdlemk4  41859  cdlemk5a  41860  cdlemk9  41864  cdlemk9bN  41865  cdlemk10  41868  cdlemk30  41919  cdlemk31  41921  cdlemk39  41941  cdlemkfid1N  41946  cdlemkfid2N  41948  cdlemk19ylem  41955  cdlemk19xlem  41967  cdlemk53b  41981  cdlemk53  41982  cdlemk55a  41984  cdlemk43N  41988  cdlemk19u1  41994  cdlemm10N  42143  cdlemn2  42220  cdlemn10  42231  dihjustlem  42241  dihord2cN  42246  dihvalcq2  42272  dihopelvalcpre  42273  dihord5b  42284  dihord6b  42285  dihmeetlem2N  42324  dihmeetbclemN  42329  dihmeetlem4preN  42331  dihmeetALTN  42352  dochshpncl  42409  dochsatshpb  42477  hdmapval3N  42863  hgmap11  42927  remulcand  43458  pellfundex  43846  congtr  43925  fzmaxdif  43941  isnumbasgrplem2  44064  idomsubgmo  44153  ntrclsk13  45030  grumnudlem  45228  restuni3  46076  unirnmapsn  46170  ssmapsn  46172  infnsuprnmpt  46205  upbdrech  46264  suplesup  46295  infleinf  46327  supxrunb3  46354  mullimc  46572  islptre  46575  mullimcf  46579  neglimc  46601  limsupmnfuzlem  46680  limsupre3lem  46686  limsupre3uzlem  46689  icccncfext  46841  dvmptfprod  46899  stoweidlem31  46985  opnvonmbllem2  47587  smflimsuplem7  47780  ormkglobd  47831  funressneu  48061  cfsetsnfsetf1  48073  prmdvdsfmtnof1lem1  48613  uhgrimisgrgriclem  48972  clnbgrgrim  48976  grlimedgclnbgr  49037  domnmsuppn0  49425  lincext3  49512  2arymaptfo  49710