Theorem simp1r 1195

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

Syntax hints:   → wi 4   ∧ wa 399   ∧ w3a 1084

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 210  df-an 400  df-3an 1086

This theorem is referenced by:  simp11r  1282  simp21r  1288  simp31r  1294  offsplitfpar  7798  omeulem2  8192  uniinqs  8360  unxpdomlem3  8708  elfiun  8878  cofsmo  9680  isfin2-2  9730  isf32lem9  9772  tskun  10197  tskurn  10200  reclem3pr  10460  dedekind  10792  subaddmulsub  11092  dmdcan  11339  lt2msq1  11513  supmullem1  11598  supmul  11600  xaddass2  12631  xlt2add  12641  xmulasslem3  12667  iccsplit  12863  expaddzlem  13468  expaddz  13469  expmulz  13471  limsupgle  14826  o1add  14962  o1mul  14963  o1sub  14964  bitsfzo  15774  sadfval  15791  smufval  15816  prmexpb  16052  4sqlem18  16288  vdwlem10  16316  setsstruct2  16513  mrieqv2d  16902  curf1  17467  mgmsscl  17849  mndodcong  18662  subgabl  18949  gex2abl  18964  cntzsubr  19561  abvres  19603  lbsind2  19846  lbsextlem2  19924  lbsextg  19927  matring  21048  mdetunilem8  21224  maducoeval  21244  maducoeval2  21245  madurid  21249  cramerimplem3  21290  pmatcollpw2  21383  pm2mpf1  21404  cnprest  21894  isreg2  21982  fbssfi  22442  hausflimlem  22584  tmdgsum  22700  ssblps  23029  ssbl  23030  xrsmopn  23417  cphassi  23819  cphassir  23820  4cphipval2  23846  cphipval  23847  dvres2  24515  vieta1  24908  aalioulem4  24931  efgh  25133  cxpadd  25270  cxpsub  25273  divcxp  25278  cxple2  25288  cxplt2  25289  cxpcn3lem  25336  angcan  25388  ang180lem5  25399  isosctrlem3  25406  lgssq  25921  brbtwn2  26699  axcontlem4  26761  axcontlem8  26765  uhgr2edg  26998  chscllem4  29423  cshwrnid  30661  ogrpinvlt  30774  pstmval  31248  measinblem  31589  cvmlift2lem6  32668  eqfunresadj  33117  poseq  33208  noetalem5  33334  linethru  33727  cnres2  35201  lcv1  36337  lfl1  36366  lshpkrex  36414  hlrelat3  36708  cvrval3  36709  cvrval4N  36710  athgt  36752  atcvrlln2  36815  atcvrlln  36816  lvolnle3at  36878  lvolnlelpln  36881  4atlem11  36905  4atlem12  36908  2lplnj  36916  dalemddea  36980  cdlema2N  37088  paddasslem2  37117  atmod1i1m  37154  lhp2lt  37297  lhp0lt  37299  lhpexle3lem  37307  lhpj1  37318  lhpmcvr4N  37322  lhpelim  37333  lhpmod2i2  37334  lhpmod6i1  37335  cdlemb2  37337  lhpat  37339  ltrnatb  37433  ltrnel  37435  ltrncnvel  37438  ltrncnv  37442  trlval2  37459  trljat1  37462  trljat2  37463  trlnidatb  37473  cdlemc1  37487  cdlemc2  37488  cdlemc5  37491  cdlemc6  37492  cdleme0aa  37506  cdleme0b  37508  cdleme0c  37509  cdleme0e  37513  cdleme0fN  37514  cdleme01N  37517  cdleme0ex1N  37519  cdleme0moN  37521  cdleme3g  37530  cdleme3h  37531  cdleme3  37533  cdleme4  37534  cdleme4a  37535  cdleme5  37536  cdleme8  37546  cdleme9  37549  cdleme10  37550  cdleme16aN  37555  cdleme11fN  37560  cdleme11g  37561  cdleme11k  37564  cdleme13  37568  cdleme17c  37584  cdleme17d1  37585  cdleme18c  37589  cdleme22gb  37590  cdlemeda  37594  cdlemednpq  37595  cdlemednuN  37596  cdleme19c  37601  cdleme20aN  37605  cdleme20bN  37606  cdleme20c  37607  cdleme22aa  37635  cdleme22d  37639  cdleme22e  37640  cdleme27cl  37662  cdleme27a  37663  cdleme30a  37674  cdleme42a  37767  cdleme42c  37768  cdlemg2fv2  37896  cdlemg2m  37900  cdlemg4g  37912  cdlemg4  37913  cdlemg6c  37916  cdlemg7aN  37921  cdlemg9a  37928  cdlemg9b  37929  cdlemg10c  37935  cdlemg12a  37939  cdlemg12b  37940  cdlemg17a  37957  cdlemg18b  37975  cdlemg18c  37976  trlcoabs2N  38018  trlcolem  38022  tendoco2  38064  tendoicl  38092  cdlemi1  38114  cdlemi2  38115  cdlemj3  38119  tendocan  38120  cdlemk3  38129  cdlemk4  38130  cdlemk5a  38131  cdlemk9  38135  cdlemk9bN  38136  cdlemk10  38139  cdlemk30  38190  cdlemk31  38192  cdlemk39  38212  cdlemkfid1N  38217  cdlemkfid2N  38219  cdlemk19ylem  38226  cdlemk19xlem  38238  cdlemk53b  38252  cdlemk53  38253  cdlemk55a  38255  cdlemk43N  38259  cdlemk19u1  38265  cdlemm10N  38414  cdlemn2  38491  cdlemn10  38502  dihjustlem  38512  dihord2cN  38517  dihvalcq2  38543  dihopelvalcpre  38544  dihord5b  38555  dihord6b  38556  dihmeetlem2N  38595  dihmeetbclemN  38600  dihmeetlem4preN  38602  dihmeetALTN  38623  dochshpncl  38680  dochsatshpb  38748  hdmapval3N  39134  hgmap11  39198  nn0rppwr  39490  remulcand  39575  pellfundex  39827  congtr  39906  fzmaxdif  39922  isnumbasgrplem2  40048  idomsubgmo  40142  ntrclsk13  40774  grumnudlem  40993  restuni3  41753  unirnmapsn  41843  ssmapsn  41845  infnsuprnmpt  41888  upbdrech  41937  suplesup  41971  infleinf  42004  supxrunb3  42036  mullimc  42258  islptre  42261  mullimcf  42265  neglimc  42289  limsupmnfuzlem  42368  limsupre3lem  42374  limsupre3uzlem  42377  icccncfext  42529  dvmptfprod  42587  stoweidlem31  42673  opnvonmbllem2  43272  smflimsuplem7  43457  funressneu  43639  prmdvdsfmtnof1lem1  44101  domnmsuppn0  44771  mndpfsupp  44778  lincext3  44865  2arymaptfo  45068