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

Syntax hints:   → wi 4   ∧ wa 395   ∧ 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 207  df-an 396  df-3an 1089

This theorem is referenced by:  simp11r  1286  simp21r  1292  simp31r  1298  eqfunresadj  7380  offsplitfpar  8144  poseq  8183  omeulem2  8621  uniinqs  8837  unxpdomlem3  9288  elfiun  9470  cofsmo  10309  isfin2-2  10359  isf32lem9  10401  tskun  10826  tskurn  10829  reclem3pr  11089  dedekind  11424  subaddmulsub  11726  dmdcan  11977  lt2msq1  12152  supmullem1  12238  supmul  12240  xaddass2  13292  xlt2add  13302  xmulasslem3  13328  iccsplit  13525  expaddzlem  14146  expaddz  14147  expmulz  14149  limsupgle  15513  o1add  15650  o1mul  15651  o1sub  15652  bitsfzo  16472  sadfval  16489  smufval  16514  nn0rppwr  16598  prmexpb  16756  4sqlem18  17000  vdwlem10  17028  setsstruct2  17211  mrieqv2d  17682  curf1  18270  mgmsscl  18658  mndpfsupp  18780  mndodcong  19560  subgabl  19854  gex2abl  19869  cntzsubrng  20567  cntzsubr  20606  abvres  20832  lbsind2  21080  lbsextlem2  21161  lbsextg  21164  matring  22449  mdetunilem8  22625  maducoeval  22645  maducoeval2  22646  madurid  22650  cramerimplem3  22691  pmatcollpw2  22784  pm2mpf1  22805  cnprest  23297  isreg2  23385  fbssfi  23845  hausflimlem  23987  tmdgsum  24103  ssblps  24432  ssbl  24433  xrsmopn  24834  cphassi  25248  cphassir  25249  4cphipval2  25276  cphipval  25277  dvres2  25947  vieta1  26354  aalioulem4  26377  efgh  26583  cxpadd  26721  cxpsub  26724  divcxp  26729  cxple2  26739  cxplt2  26740  cxpcn3lem  26790  angcan  26845  ang180lem5  26856  isosctrlem3  26863  lgssq  27381  nosupinfsep  27777  noetalem1  27786  noeta2  27829  sltlpss  27945  brbtwn2  28920  axcontlem4  28982  axcontlem8  28986  uhgr2edg  29225  chscllem4  31659  cshwrnid  32946  ogrpinvlt  33100  pstmval  33894  measinblem  34221  cvmlift2lem6  35313  linethru  36154  cnres2  37770  lcv1  39042  lfl1  39071  lshpkrex  39119  hlrelat3  39414  cvrval3  39415  cvrval4N  39416  athgt  39458  atcvrlln2  39521  atcvrlln  39522  lvolnle3at  39584  lvolnlelpln  39587  4atlem11  39611  4atlem12  39614  2lplnj  39622  dalemddea  39686  cdlema2N  39794  paddasslem2  39823  atmod1i1m  39860  lhp2lt  40003  lhp0lt  40005  lhpexle3lem  40013  lhpj1  40024  lhpmcvr4N  40028  lhpelim  40039  lhpmod2i2  40040  lhpmod6i1  40041  cdlemb2  40043  lhpat  40045  ltrnatb  40139  ltrnel  40141  ltrncnvel  40144  ltrncnv  40148  trlval2  40165  trljat1  40168  trljat2  40169  trlnidatb  40179  cdlemc1  40193  cdlemc2  40194  cdlemc5  40197  cdlemc6  40198  cdleme0aa  40212  cdleme0b  40214  cdleme0c  40215  cdleme0e  40219  cdleme0fN  40220  cdleme01N  40223  cdleme0ex1N  40225  cdleme0moN  40227  cdleme3g  40236  cdleme3h  40237  cdleme3  40239  cdleme4  40240  cdleme4a  40241  cdleme5  40242  cdleme8  40252  cdleme9  40255  cdleme10  40256  cdleme16aN  40261  cdleme11fN  40266  cdleme11g  40267  cdleme11k  40270  cdleme13  40274  cdleme17c  40290  cdleme17d1  40291  cdleme18c  40295  cdleme22gb  40296  cdlemeda  40300  cdlemednpq  40301  cdlemednuN  40302  cdleme19c  40307  cdleme20aN  40311  cdleme20bN  40312  cdleme20c  40313  cdleme22aa  40341  cdleme22d  40345  cdleme22e  40346  cdleme27cl  40368  cdleme27a  40369  cdleme30a  40380  cdleme42a  40473  cdleme42c  40474  cdlemg2fv2  40602  cdlemg2m  40606  cdlemg4g  40618  cdlemg4  40619  cdlemg6c  40622  cdlemg7aN  40627  cdlemg9a  40634  cdlemg9b  40635  cdlemg10c  40641  cdlemg12a  40645  cdlemg12b  40646  cdlemg17a  40663  cdlemg18b  40681  cdlemg18c  40682  trlcoabs2N  40724  trlcolem  40728  tendoco2  40770  tendoicl  40798  cdlemi1  40820  cdlemi2  40821  cdlemj3  40825  tendocan  40826  cdlemk3  40835  cdlemk4  40836  cdlemk5a  40837  cdlemk9  40841  cdlemk9bN  40842  cdlemk10  40845  cdlemk30  40896  cdlemk31  40898  cdlemk39  40918  cdlemkfid1N  40923  cdlemkfid2N  40925  cdlemk19ylem  40932  cdlemk19xlem  40944  cdlemk53b  40958  cdlemk53  40959  cdlemk55a  40961  cdlemk43N  40965  cdlemk19u1  40971  cdlemm10N  41120  cdlemn2  41197  cdlemn10  41208  dihjustlem  41218  dihord2cN  41223  dihvalcq2  41249  dihopelvalcpre  41250  dihord5b  41261  dihord6b  41262  dihmeetlem2N  41301  dihmeetbclemN  41306  dihmeetlem4preN  41308  dihmeetALTN  41329  dochshpncl  41386  dochsatshpb  41454  hdmapval3N  41840  hgmap11  41904  f1o2d2  42274  remulcand  42468  pellfundex  42897  congtr  42977  fzmaxdif  42993  isnumbasgrplem2  43116  idomsubgmo  43205  ntrclsk13  44084  grumnudlem  44304  restuni3  45123  unirnmapsn  45219  ssmapsn  45221  infnsuprnmpt  45257  upbdrech  45317  suplesup  45350  infleinf  45383  supxrunb3  45410  mullimc  45631  islptre  45634  mullimcf  45638  neglimc  45662  limsupmnfuzlem  45741  limsupre3lem  45747  limsupre3uzlem  45750  icccncfext  45902  dvmptfprod  45960  stoweidlem31  46046  opnvonmbllem2  46648  smflimsuplem7  46841  ormkglobd  46890  funressneu  47059  cfsetsnfsetf1  47071  prmdvdsfmtnof1lem1  47571  uhgrimisgrgriclem  47898  clnbgrgrim  47902  domnmsuppn0  48285  lincext3  48373  2arymaptfo  48575