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 1133	1 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒 ∧ 𝜃) → 𝜓)

Syntax hints:   → wi 4   ∧ wa 395   ∧ w3a 1086

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 1088

This theorem is referenced by:  simp11r  1286  simp21r  1292  simp31r  1298  eqfunresadj  7338  offsplitfpar  8101  poseq  8140  omeulem2  8550  uniinqs  8773  unxpdomlem3  9206  elfiun  9388  cofsmo  10229  isfin2-2  10279  isf32lem9  10321  tskun  10746  tskurn  10749  reclem3pr  11009  dedekind  11344  subaddmulsub  11648  dmdcan  11899  lt2msq1  12074  supmullem1  12160  supmul  12162  xaddass2  13217  xlt2add  13227  xmulasslem3  13253  iccsplit  13453  expaddzlem  14077  expaddz  14078  expmulz  14080  limsupgle  15450  o1add  15587  o1mul  15588  o1sub  15589  bitsfzo  16412  sadfval  16429  smufval  16454  nn0rppwr  16538  prmexpb  16696  4sqlem18  16940  vdwlem10  16968  setsstruct2  17151  mrieqv2d  17607  curf1  18193  mgmsscl  18579  mndpfsupp  18701  mndodcong  19479  subgabl  19773  gex2abl  19788  cntzsubrng  20483  cntzsubr  20522  abvres  20747  lbsind2  20995  lbsextlem2  21076  lbsextg  21079  matring  22337  mdetunilem8  22513  maducoeval  22533  maducoeval2  22534  madurid  22538  cramerimplem3  22579  pmatcollpw2  22672  pm2mpf1  22693  cnprest  23183  isreg2  23271  fbssfi  23731  hausflimlem  23873  tmdgsum  23989  ssblps  24317  ssbl  24318  xrsmopn  24708  cphassi  25121  cphassir  25122  4cphipval2  25149  cphipval  25150  dvres2  25820  vieta1  26227  aalioulem4  26250  efgh  26457  cxpadd  26595  cxpsub  26598  divcxp  26603  cxple2  26613  cxplt2  26614  cxpcn3lem  26664  angcan  26719  ang180lem5  26730  isosctrlem3  26737  lgssq  27255  nosupinfsep  27651  noetalem1  27660  noeta2  27703  sltlpss  27826  brbtwn2  28839  axcontlem4  28901  axcontlem8  28905  uhgr2edg  29142  chscllem4  31576  cshwrnid  32890  ogrpinvlt  33044  pstmval  33892  measinblem  34217  cvmlift2lem6  35302  linethru  36148  cnres2  37764  lcv1  39041  lfl1  39070  lshpkrex  39118  hlrelat3  39413  cvrval3  39414  cvrval4N  39415  athgt  39457  atcvrlln2  39520  atcvrlln  39521  lvolnle3at  39583  lvolnlelpln  39586  4atlem11  39610  4atlem12  39613  2lplnj  39621  dalemddea  39685  cdlema2N  39793  paddasslem2  39822  atmod1i1m  39859  lhp2lt  40002  lhp0lt  40004  lhpexle3lem  40012  lhpj1  40023  lhpmcvr4N  40027  lhpelim  40038  lhpmod2i2  40039  lhpmod6i1  40040  cdlemb2  40042  lhpat  40044  ltrnatb  40138  ltrnel  40140  ltrncnvel  40143  ltrncnv  40147  trlval2  40164  trljat1  40167  trljat2  40168  trlnidatb  40178  cdlemc1  40192  cdlemc2  40193  cdlemc5  40196  cdlemc6  40197  cdleme0aa  40211  cdleme0b  40213  cdleme0c  40214  cdleme0e  40218  cdleme0fN  40219  cdleme01N  40222  cdleme0ex1N  40224  cdleme0moN  40226  cdleme3g  40235  cdleme3h  40236  cdleme3  40238  cdleme4  40239  cdleme4a  40240  cdleme5  40241  cdleme8  40251  cdleme9  40254  cdleme10  40255  cdleme16aN  40260  cdleme11fN  40265  cdleme11g  40266  cdleme11k  40269  cdleme13  40273  cdleme17c  40289  cdleme17d1  40290  cdleme18c  40294  cdleme22gb  40295  cdlemeda  40299  cdlemednpq  40300  cdlemednuN  40301  cdleme19c  40306  cdleme20aN  40310  cdleme20bN  40311  cdleme20c  40312  cdleme22aa  40340  cdleme22d  40344  cdleme22e  40345  cdleme27cl  40367  cdleme27a  40368  cdleme30a  40379  cdleme42a  40472  cdleme42c  40473  cdlemg2fv2  40601  cdlemg2m  40605  cdlemg4g  40617  cdlemg4  40618  cdlemg6c  40621  cdlemg7aN  40626  cdlemg9a  40633  cdlemg9b  40634  cdlemg10c  40640  cdlemg12a  40644  cdlemg12b  40645  cdlemg17a  40662  cdlemg18b  40680  cdlemg18c  40681  trlcoabs2N  40723  trlcolem  40727  tendoco2  40769  tendoicl  40797  cdlemi1  40819  cdlemi2  40820  cdlemj3  40824  tendocan  40825  cdlemk3  40834  cdlemk4  40835  cdlemk5a  40836  cdlemk9  40840  cdlemk9bN  40841  cdlemk10  40844  cdlemk30  40895  cdlemk31  40897  cdlemk39  40917  cdlemkfid1N  40922  cdlemkfid2N  40924  cdlemk19ylem  40931  cdlemk19xlem  40943  cdlemk53b  40957  cdlemk53  40958  cdlemk55a  40960  cdlemk43N  40964  cdlemk19u1  40970  cdlemm10N  41119  cdlemn2  41196  cdlemn10  41207  dihjustlem  41217  dihord2cN  41222  dihvalcq2  41248  dihopelvalcpre  41249  dihord5b  41260  dihord6b  41261  dihmeetlem2N  41300  dihmeetbclemN  41305  dihmeetlem4preN  41307  dihmeetALTN  41328  dochshpncl  41385  dochsatshpb  41453  hdmapval3N  41839  hgmap11  41903  f1o2d2  42228  remulcand  42434  pellfundex  42881  congtr  42961  fzmaxdif  42977  isnumbasgrplem2  43100  idomsubgmo  43189  ntrclsk13  44067  grumnudlem  44281  restuni3  45119  unirnmapsn  45215  ssmapsn  45217  infnsuprnmpt  45251  upbdrech  45310  suplesup  45342  infleinf  45375  supxrunb3  45402  mullimc  45621  islptre  45624  mullimcf  45628  neglimc  45652  limsupmnfuzlem  45731  limsupre3lem  45737  limsupre3uzlem  45740  icccncfext  45892  dvmptfprod  45950  stoweidlem31  46036  opnvonmbllem2  46638  smflimsuplem7  46831  ormkglobd  46880  funressneu  47052  cfsetsnfsetf1  47064  prmdvdsfmtnof1lem1  47589  uhgrimisgrgriclem  47934  clnbgrgrim  47938  domnmsuppn0  48361  lincext3  48449  2arymaptfo  48647