Theorem simp1r 1212

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

Syntax hints:   → wi 4   ∧ wa 386   ∧ w3a 1071

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 199  df-an 387  df-3an 1073

This theorem is referenced by:  simpl1rOLD  1253  simpr1rOLD  1265  simp11r  1341  simp21r  1347  simp31r  1353  omeulem2  7947  uniinqs  8110  unxpdomlem3  8454  elfiun  8624  cofsmo  9426  isfin2-2  9476  isf32lem9  9518  tskun  9943  tskurn  9946  reclem3pr  10206  dedekind  10539  subaddmulsub  10838  dmdcan  11085  lt2msq1  11261  supmullem1  11347  supmul  11349  xaddass2  12392  xlt2add  12402  xmulasslem3  12428  iccsplit  12622  expaddzlem  13221  expaddz  13222  expmulz  13224  limsupgle  14616  o1add  14752  o1mul  14753  o1sub  14754  bitsfzo  15563  sadfval  15580  smufval  15605  prmexpb  15834  4sqlem18  16070  vdwlem10  16098  setsstruct2  16293  mrieqv2d  16685  curf1  17251  mndodcong  18345  subgabl  18627  gex2abl  18640  cntzsubr  19204  abvres  19231  lbsind2  19476  lbsextlem2  19556  lbsextg  19559  matring  20653  mdetunilem8  20830  maducoeval  20850  maducoeval2  20851  madurid  20855  cramerimplem3  20898  pmatcollpw2  20990  pm2mpf1  21011  cnprest  21501  isreg2  21589  fbssfi  22049  hausflimlem  22191  tmdgsum  22307  ssblps  22635  ssbl  22636  xrsmopn  23023  cphassi  23421  cphassir  23422  4cphipval2  23448  cphipval  23449  dvres2  24113  vieta1  24504  aalioulem4  24527  efgh  24725  cxpadd  24862  cxpsub  24865  divcxp  24870  cxple2  24880  cxplt2  24881  cxpcn3lem  24928  angcan  24980  ang180lem5  24991  isosctrlem3  24998  lgssq  25514  brbtwn2  26254  axcontlem4  26316  axcontlem8  26320  uhgr2edg  26554  chscllem4  29071  ogrpinvlt  30286  pstmval  30536  measinblem  30881  cvmlift2lem6  31889  eqfunresadj  32252  poseq  32342  noetalem5  32456  linethru  32849  cnres2  34170  lcv1  35179  lfl1  35208  lshpkrex  35256  hlrelat3  35550  cvrval3  35551  cvrval4N  35552  athgt  35594  atcvrlln2  35657  atcvrlln  35658  lvolnle3at  35720  lvolnlelpln  35723  4atlem11  35747  4atlem12  35750  2lplnj  35758  dalemddea  35822  cdlema2N  35930  paddasslem2  35959  atmod1i1m  35996  lhp2lt  36139  lhp0lt  36141  lhpexle3lem  36149  lhpj1  36160  lhpmcvr4N  36164  lhpelim  36175  lhpmod2i2  36176  lhpmod6i1  36177  cdlemb2  36179  lhpat  36181  ltrnatb  36275  ltrnel  36277  ltrncnvel  36280  ltrncnv  36284  trlval2  36301  trljat1  36304  trljat2  36305  trlnidatb  36315  cdlemc1  36329  cdlemc2  36330  cdlemc5  36333  cdlemc6  36334  cdleme0aa  36348  cdleme0b  36350  cdleme0c  36351  cdleme0e  36355  cdleme0fN  36356  cdleme01N  36359  cdleme0ex1N  36361  cdleme0moN  36363  cdleme3g  36372  cdleme3h  36373  cdleme3  36375  cdleme4  36376  cdleme4a  36377  cdleme5  36378  cdleme8  36388  cdleme9  36391  cdleme10  36392  cdleme16aN  36397  cdleme11fN  36402  cdleme11g  36403  cdleme11k  36406  cdleme13  36410  cdleme17c  36426  cdleme17d1  36427  cdleme18c  36431  cdleme22gb  36432  cdlemeda  36436  cdlemednpq  36437  cdlemednuN  36438  cdleme19c  36443  cdleme20aN  36447  cdleme20bN  36448  cdleme20c  36449  cdleme22aa  36477  cdleme22d  36481  cdleme22e  36482  cdleme27cl  36504  cdleme27a  36505  cdleme30a  36516  cdleme42a  36609  cdleme42c  36610  cdlemg2fv2  36738  cdlemg2m  36742  cdlemg4g  36754  cdlemg4  36755  cdlemg6c  36758  cdlemg7aN  36763  cdlemg9a  36770  cdlemg9b  36771  cdlemg10c  36777  cdlemg12a  36781  cdlemg12b  36782  cdlemg17a  36799  cdlemg18b  36817  cdlemg18c  36818  trlcoabs2N  36860  trlcolem  36864  tendoco2  36906  tendoicl  36934  cdlemi1  36956  cdlemi2  36957  cdlemj3  36961  tendocan  36962  cdlemk3  36971  cdlemk4  36972  cdlemk5a  36973  cdlemk9  36977  cdlemk9bN  36978  cdlemk10  36981  cdlemk30  37032  cdlemk31  37034  cdlemk39  37054  cdlemkfid1N  37059  cdlemkfid2N  37061  cdlemk19ylem  37068  cdlemk19xlem  37080  cdlemk53b  37094  cdlemk53  37095  cdlemk55a  37097  cdlemk43N  37101  cdlemk19u1  37107  cdlemm10N  37256  cdlemn2  37333  cdlemn10  37344  dihjustlem  37354  dihord2cN  37359  dihvalcq2  37385  dihopelvalcpre  37386  dihord5b  37397  dihord6b  37398  dihmeetlem2N  37437  dihmeetbclemN  37442  dihmeetlem4preN  37444  dihmeetALTN  37465  dochshpncl  37522  dochsatshpb  37590  hdmapval3N  37976  hgmap11  38040  nn0rppwr  38144  pellfundex  38392  congtr  38473  fzmaxdif  38489  isnumbasgrplem2  38615  idomsubgmo  38717  ntrclsk13  39307  restuni3  40212  unirnmapsn  40309  ssmapsn  40311  infnsuprnmpt  40358  upbdrech  40410  suplesup  40445  infleinf  40478  supxrunb3  40511  mullimc  40738  islptre  40741  mullimcf  40745  neglimc  40769  limsupmnfuzlem  40848  limsupre3lem  40854  limsupre3uzlem  40857  icccncfext  41010  dvmptfprod  41070  stoweidlem31  41157  opnvonmbllem2  41756  smflimsuplem7  41941  funressneu  42094  prmdvdsfmtnof1lem1  42499  domnmsuppn0  43147  mndpfsupp  43154  lincext3  43242