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  7396  offsplitfpar  8160  mpof1o2d  8167  poseq  8205  omeulem2  8622  uniinqs  8849  unxpdomlem3  9280  elfiun  9452  cofsmo  10377  isfin2-2  10427  isf32lem9  10469  tskun  10901  tskurn  10904  reclem3pr  11164  dedekind  11503  subaddmulsub  11809  dmdcan  12057  lt2msq1  12231  supmullem1  12317  supmul  12319  xaddass2  13410  xlt2add  13420  xmulasslem3  13446  iccsplit  13646  expaddzlem  14278  expaddz  14279  expmulz  14281  limsupgle  15676  o1add  15813  o1mul  15814  o1sub  15815  bitsfzo  16637  sadfval  16654  smufval  16679  nn0rppwr  16767  prmexpb  16927  4sqlem18  17172  vdwlem10  17200  setsstruct2  17384  mrieqv2d  17845  curf1  18431  chnccat  18832  mgmsscl  18853  mndpfsupp  18993  mndodcong  19789  subgabl  20083  gex2abl  20098  ogrpinvlt  20391  rng1zrlem  20436  cntzsubrng  20852  cntzsubr  20891  abvres  21121  lbsind2  21389  lbsextlem2  21470  lbsextg  21473  matring  22791  mdetunilem8  22967  maducoeval  22987  maducoeval2  22988  madurid  22992  cramerimplem3  23036  pmatcollpw2  23129  pm2mpf1  23150  cnprest  23640  isreg2  23728  fbssfi  24189  hausflimlem  24331  tmdgsum  24447  ssblps  24774  ssbl  24775  xrsmopn  25165  cphassi  25568  cphassir  25569  4cphipval2  25596  cphipval  25597  dvres2  26265  vieta1  26668  aalioulem4  26695  efgh  26902  cxpadd  27040  cxpsub  27043  divcxp  27048  cxple2  27058  cxplt2  27059  cxpcn3lem  27108  angcan  27163  ang180lem5  27174  isosctrlem3  27181  lgssq  27697  nosupinfsep  28122  noetalem1  28131  noeta2  28180  ltslpss  28327  bdayfinbndlem1  28886  brbtwn2  29516  axcontlem4  29578  axcontlem8  29582  uhgr2edg  29822  chscllem4  32275  cshwrnid  33595  pstmval  34610  measinblem  34936  cvmlift2lem6  36253  linethru  37109  cnres2  38900  lcv1  40301  lfl1  40330  lshpkrex  40378  hlrelat3  40672  cvrval3  40673  cvrval4N  40674  athgt  40716  atcvrlln2  40779  atcvrlln  40780  lvolnle3at  40842  lvolnlelpln  40845  4atlem11  40869  4atlem12  40872  2lplnj  40880  dalemddea  40944  cdlema2N  41052  paddasslem2  41081  atmod1i1m  41118  lhp2lt  41261  lhp0lt  41263  lhpexle3lem  41271  lhpj1  41282  lhpmcvr4N  41286  lhpelim  41297  lhpmod2i2  41298  lhpmod6i1  41299  cdlemb2  41301  lhpat  41303  ltrnatb  41397  ltrnel  41399  ltrncnvel  41402  ltrncnv  41406  trlval2  41423  trljat1  41426  trljat2  41427  trlnidatb  41437  cdlemc1  41451  cdlemc2  41452  cdlemc5  41455  cdlemc6  41456  cdleme0aa  41470  cdleme0b  41472  cdleme0c  41473  cdleme0e  41477  cdleme0fN  41478  cdleme01N  41481  cdleme0ex1N  41483  cdleme0moN  41485  cdleme3g  41494  cdleme3h  41495  cdleme3  41497  cdleme4  41498  cdleme4a  41499  cdleme5  41500  cdleme8  41510  cdleme9  41513  cdleme10  41514  cdleme16aN  41519  cdleme11fN  41524  cdleme11g  41525  cdleme11k  41528  cdleme13  41532  cdleme17c  41548  cdleme17d1  41549  cdleme18c  41553  cdleme22gb  41554  cdlemeda  41558  cdlemednpq  41559  cdlemednuN  41560  cdleme19c  41565  cdleme20aN  41569  cdleme20bN  41570  cdleme20c  41571  cdleme22aa  41599  cdleme22d  41603  cdleme22e  41604  cdleme27cl  41626  cdleme27a  41627  cdleme30a  41638  cdleme42a  41731  cdleme42c  41732  cdlemg2fv2  41860  cdlemg2m  41864  cdlemg4g  41876  cdlemg4  41877  cdlemg6c  41880  cdlemg7aN  41885  cdlemg9a  41892  cdlemg9b  41893  cdlemg10c  41899  cdlemg12a  41903  cdlemg12b  41904  cdlemg17a  41921  cdlemg18b  41939  cdlemg18c  41940  trlcoabs2N  41982  trlcolem  41986  tendoco2  42028  tendoicl  42056  cdlemi1  42078  cdlemi2  42079  cdlemj3  42083  tendocan  42084  cdlemk3  42093  cdlemk4  42094  cdlemk5a  42095  cdlemk9  42099  cdlemk9bN  42100  cdlemk10  42103  cdlemk30  42154  cdlemk31  42156  cdlemk39  42176  cdlemkfid1N  42181  cdlemkfid2N  42183  cdlemk19ylem  42190  cdlemk19xlem  42202  cdlemk53b  42216  cdlemk53  42217  cdlemk55a  42219  cdlemk43N  42223  cdlemk19u1  42229  cdlemm10N  42378  cdlemn2  42455  cdlemn10  42466  dihjustlem  42476  dihord2cN  42481  dihvalcq2  42507  dihopelvalcpre  42508  dihord5b  42519  dihord6b  42520  dihmeetlem2N  42559  dihmeetbclemN  42564  dihmeetlem4preN  42566  dihmeetALTN  42587  dochshpncl  42644  dochsatshpb  42712  hdmapval3N  43098  hgmap11  43162  remulcand  43694  pellfundex  44097  congtr  44176  fzmaxdif  44192  isnumbasgrplem2  44309  idomsubgmo  44398  ntrclsk13  45274  grumnudlem  45472  restuni3  46348  unirnmapsn  46442  ssmapsn  46444  infnsuprnmpt  46477  upbdrech  46536  suplesup  46566  infleinf  46598  supxrunb3  46625  mullimc  46843  islptre  46846  mullimcf  46850  neglimc  46872  limsupmnfuzlem  46951  limsupre3lem  46957  limsupre3uzlem  46960  icccncfext  47112  dvmptfprod  47170  stoweidlem31  47256  opnvonmbllem2  47858  smflimsuplem7  48051  ormkglobd  48102  funressneu  48332  cfsetsnfsetf1  48344  prmdvdsfmtnof1lem1  48884  uhgrimisgrgriclem  49243  clnbgrgrim  49247  grlimedgclnbgr  49308  domnmsuppn0  49696  lincext3  49783  2arymaptfo  49981