Theorem simp1r 1196

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

Syntax hints:   → wi 4   ∧ wa 394   ∧ w3a 1085

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 206  df-an 395  df-3an 1087

This theorem is referenced by:  simp11r  1283  simp21r  1289  simp31r  1295  eqfunresadj  7359  offsplitfpar  8107  poseq  8146  omeulem2  8585  uniinqs  8793  unxpdomlem3  9254  elfiun  9427  cofsmo  10266  isfin2-2  10316  isf32lem9  10358  tskun  10783  tskurn  10786  reclem3pr  11046  dedekind  11381  subaddmulsub  11681  dmdcan  11928  lt2msq1  12102  supmullem1  12188  supmul  12190  xaddass2  13233  xlt2add  13243  xmulasslem3  13269  iccsplit  13466  expaddzlem  14075  expaddz  14076  expmulz  14078  limsupgle  15425  o1add  15562  o1mul  15563  o1sub  15564  bitsfzo  16380  sadfval  16397  smufval  16422  prmexpb  16661  4sqlem18  16899  vdwlem10  16927  setsstruct2  17111  mrieqv2d  17587  curf1  18182  mgmsscl  18570  mndodcong  19451  subgabl  19745  gex2abl  19760  cntzsubrng  20455  cntzsubr  20496  abvres  20590  lbsind2  20836  lbsextlem2  20917  lbsextg  20920  matring  22165  mdetunilem8  22341  maducoeval  22361  maducoeval2  22362  madurid  22366  cramerimplem3  22407  pmatcollpw2  22500  pm2mpf1  22521  cnprest  23013  isreg2  23101  fbssfi  23561  hausflimlem  23703  tmdgsum  23819  ssblps  24148  ssbl  24149  xrsmopn  24548  cphassi  24962  cphassir  24963  4cphipval2  24990  cphipval  24991  dvres2  25661  vieta1  26061  aalioulem4  26084  efgh  26286  cxpadd  26423  cxpsub  26426  divcxp  26431  cxple2  26441  cxplt2  26442  cxpcn3lem  26491  angcan  26543  ang180lem5  26554  isosctrlem3  26561  lgssq  27076  nosupinfsep  27471  noetalem1  27480  noeta2  27522  sltlpss  27638  brbtwn2  28430  axcontlem4  28492  axcontlem8  28496  uhgr2edg  28732  chscllem4  31160  cshwrnid  32392  ogrpinvlt  32511  pstmval  33173  measinblem  33516  cvmlift2lem6  34597  linethru  35429  cnres2  36934  lcv1  38214  lfl1  38243  lshpkrex  38291  hlrelat3  38586  cvrval3  38587  cvrval4N  38588  athgt  38630  atcvrlln2  38693  atcvrlln  38694  lvolnle3at  38756  lvolnlelpln  38759  4atlem11  38783  4atlem12  38786  2lplnj  38794  dalemddea  38858  cdlema2N  38966  paddasslem2  38995  atmod1i1m  39032  lhp2lt  39175  lhp0lt  39177  lhpexle3lem  39185  lhpj1  39196  lhpmcvr4N  39200  lhpelim  39211  lhpmod2i2  39212  lhpmod6i1  39213  cdlemb2  39215  lhpat  39217  ltrnatb  39311  ltrnel  39313  ltrncnvel  39316  ltrncnv  39320  trlval2  39337  trljat1  39340  trljat2  39341  trlnidatb  39351  cdlemc1  39365  cdlemc2  39366  cdlemc5  39369  cdlemc6  39370  cdleme0aa  39384  cdleme0b  39386  cdleme0c  39387  cdleme0e  39391  cdleme0fN  39392  cdleme01N  39395  cdleme0ex1N  39397  cdleme0moN  39399  cdleme3g  39408  cdleme3h  39409  cdleme3  39411  cdleme4  39412  cdleme4a  39413  cdleme5  39414  cdleme8  39424  cdleme9  39427  cdleme10  39428  cdleme16aN  39433  cdleme11fN  39438  cdleme11g  39439  cdleme11k  39442  cdleme13  39446  cdleme17c  39462  cdleme17d1  39463  cdleme18c  39467  cdleme22gb  39468  cdlemeda  39472  cdlemednpq  39473  cdlemednuN  39474  cdleme19c  39479  cdleme20aN  39483  cdleme20bN  39484  cdleme20c  39485  cdleme22aa  39513  cdleme22d  39517  cdleme22e  39518  cdleme27cl  39540  cdleme27a  39541  cdleme30a  39552  cdleme42a  39645  cdleme42c  39646  cdlemg2fv2  39774  cdlemg2m  39778  cdlemg4g  39790  cdlemg4  39791  cdlemg6c  39794  cdlemg7aN  39799  cdlemg9a  39806  cdlemg9b  39807  cdlemg10c  39813  cdlemg12a  39817  cdlemg12b  39818  cdlemg17a  39835  cdlemg18b  39853  cdlemg18c  39854  trlcoabs2N  39896  trlcolem  39900  tendoco2  39942  tendoicl  39970  cdlemi1  39992  cdlemi2  39993  cdlemj3  39997  tendocan  39998  cdlemk3  40007  cdlemk4  40008  cdlemk5a  40009  cdlemk9  40013  cdlemk9bN  40014  cdlemk10  40017  cdlemk30  40068  cdlemk31  40070  cdlemk39  40090  cdlemkfid1N  40095  cdlemkfid2N  40097  cdlemk19ylem  40104  cdlemk19xlem  40116  cdlemk53b  40130  cdlemk53  40131  cdlemk55a  40133  cdlemk43N  40137  cdlemk19u1  40143  cdlemm10N  40292  cdlemn2  40369  cdlemn10  40380  dihjustlem  40390  dihord2cN  40395  dihvalcq2  40421  dihopelvalcpre  40422  dihord5b  40433  dihord6b  40434  dihmeetlem2N  40473  dihmeetbclemN  40478  dihmeetlem4preN  40480  dihmeetALTN  40501  dochshpncl  40558  dochsatshpb  40626  hdmapval3N  41012  hgmap11  41076  f1o2d2  41361  nn0rppwr  41526  remulcand  41613  pellfundex  41926  congtr  42006  fzmaxdif  42022  isnumbasgrplem2  42148  idomsubgmo  42242  ntrclsk13  43124  grumnudlem  43346  restuni3  44108  unirnmapsn  44211  ssmapsn  44213  infnsuprnmpt  44252  upbdrech  44313  suplesup  44347  infleinf  44380  supxrunb3  44407  mullimc  44630  islptre  44633  mullimcf  44637  neglimc  44661  limsupmnfuzlem  44740  limsupre3lem  44746  limsupre3uzlem  44749  icccncfext  44901  dvmptfprod  44959  stoweidlem31  45045  opnvonmbllem2  45647  smflimsuplem7  45840  funressneu  46055  cfsetsnfsetf1  46067  prmdvdsfmtnof1lem1  46550  domnmsuppn0  47133  mndpfsupp  47140  lincext3  47224  2arymaptfo  47427