Theorem simp1r 1079

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

Syntax hints:   → wi 4   ∧ wa 383   ∧ w3a 1031

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 196  df-an 385  df-3an 1033

This theorem is referenced by:  simpl1r  1106  simpr1r  1112  simp11r  1166  simp21r  1172  simp31r  1178  vtoclgftOLD  3228  funprgOLD  5855  omeulem2  7550  uniinqs  7714  unxpdomlem3  8051  elfiun  8219  cofsmo  8974  isfin2-2  9024  isf32lem9  9066  tskun  9487  tskurn  9490  reclem3pr  9750  dedekind  10079  dmdcan  10614  lt2msq1  10786  supmullem1  10870  supmul  10872  xaddass2  11952  xlt2add  11962  xmulasslem3  11988  iccsplit  12176  expaddzlem  12765  expaddz  12766  expmulz  12768  limsupgle  14056  o1add  14192  o1mul  14193  o1sub  14194  bitsfzo  14995  sadfval  15012  smufval  15037  prmexpb  15268  4sqlem18  15504  vdwlem10  15532  mrieqv2d  16122  curf1  16688  mndodcong  17784  subgabl  18064  gex2abl  18077  cntzsubr  18635  abvres  18662  lbsind2  18902  lbsextlem2  18980  lbsextg  18983  matring  20068  mdetunilem8  20244  maducoeval  20264  maducoeval2  20265  madurid  20269  cramerimplem3  20310  pmatcollpw2  20402  pm2mpf1  20423  cnprest  20903  isreg2  20991  fbssfi  21451  hausflimlem  21593  tmdgsum  21709  ssblps  22037  ssbl  22038  xrsmopn  22423  cphassi  22822  cphassir  22823  4cphipval2  22849  cphipval  22850  dvres2  23482  vieta1  23871  aalioulem4  23894  efgh  24091  cxpadd  24225  cxpsub  24228  divcxp  24233  cxple2  24243  cxplt2  24244  cxpcn3lem  24288  angcan  24332  ang180lem5  24343  isosctrlem3  24350  lgssq  24862  brbtwn2  25585  axcontlem4  25647  axcontlem8  25651  clwwlknimp  26304  chscllem4  27883  ogrpinvlt  29055  pstmval  29266  measinblem  29610  cvmlift2lem6  30544  poseq  30994  linethru  31430  cnres2  32732  lcv1  33346  lfl1  33375  lshpkrex  33423  hlrelat3  33716  cvrval3  33717  cvrval4N  33718  athgt  33760  atcvrlln2  33823  atcvrlln  33824  lvolnle3at  33886  lvolnlelpln  33889  4atlem11  33913  4atlem12  33916  2lplnj  33924  dalemddea  33988  cdlema2N  34096  paddasslem2  34125  atmod1i1m  34162  lhp2lt  34305  lhp0lt  34307  lhpexle3lem  34315  lhpj1  34326  lhpmcvr4N  34330  lhpelim  34341  lhpmod2i2  34342  lhpmod6i1  34343  cdlemb2  34345  lhpat  34347  ltrnatb  34441  ltrnel  34443  ltrncnvel  34446  ltrncnv  34450  ltrnmwOLD  34456  trlval2  34468  trljat1  34471  trljat2  34472  trlnidatb  34482  cdlemc1  34496  cdlemc2  34497  cdlemc5  34500  cdlemc6  34501  cdleme0aa  34515  cdleme0b  34517  cdleme0c  34518  cdleme0e  34522  cdleme0fN  34523  cdleme01N  34526  cdleme0ex1N  34528  cdleme0moN  34530  cdleme3g  34539  cdleme3h  34540  cdleme3  34542  cdleme4  34543  cdleme4a  34544  cdleme5  34545  cdleme8  34555  cdleme9  34558  cdleme10  34559  cdleme16aN  34564  cdleme11fN  34569  cdleme11g  34570  cdleme11k  34573  cdleme13  34577  cdleme17c  34593  cdleme17d1  34594  cdleme18c  34598  cdleme22gb  34599  cdlemeda  34603  cdlemednpq  34604  cdlemednuN  34605  cdleme19c  34611  cdleme20aN  34615  cdleme20bN  34616  cdleme20c  34617  cdleme22aa  34645  cdleme22d  34649  cdleme22e  34650  cdleme27cl  34672  cdleme27a  34673  cdleme30a  34684  cdleme42a  34777  cdleme42c  34778  cdlemg2fv2  34906  cdlemg2m  34910  cdlemg4g  34922  cdlemg4  34923  cdlemg6c  34926  cdlemg7aN  34931  cdlemg9a  34938  cdlemg9b  34939  cdlemg10c  34945  cdlemg12a  34949  cdlemg12b  34950  cdlemg17a  34967  cdlemg18b  34985  cdlemg18c  34986  trlcoabs2N  35028  trlcolem  35032  tendoco2  35074  tendoicl  35102  cdlemi1  35124  cdlemi2  35125  cdlemj3  35129  tendocan  35130  cdlemk3  35139  cdlemk4  35140  cdlemk5a  35141  cdlemk9  35145  cdlemk9bN  35146  cdlemk10  35149  cdlemk30  35200  cdlemk31  35202  cdlemk39  35222  cdlemkfid1N  35227  cdlemkfid2N  35229  cdlemk19ylem  35236  cdlemk19xlem  35248  cdlemk53b  35262  cdlemk53  35263  cdlemk55a  35265  cdlemk43N  35269  cdlemk19u1  35275  cdlemm10N  35425  cdlemn2  35502  cdlemn10  35513  dihjustlem  35523  dihord2cN  35528  dihvalcq2  35554  dihopelvalcpre  35555  dihord5b  35566  dihord6b  35567  dihmeetlem2N  35606  dihmeetbclemN  35611  dihmeetlem4preN  35613  dihmeetALTN  35634  dochshpncl  35691  dochsatshpb  35759  hdmapval3N  36148  hgmap11  36212  pellfundex  36468  congtr  36550  fzmaxdif  36566  isnumbasgrplem2  36693  idomsubgmo  36795  ntrclsk13  37389  restuni3  38333  unirnmapsn  38401  ssmapsn  38403  upbdrech  38460  suplesup  38496  infleinf  38529  mullimc  38683  islptre  38686  mullimcf  38690  neglimc  38714  icccncfext  38773  dvmptfprod  38835  stoweidlem31  38924  opnvonmbllem2  39523  prmdvdsfmtnof1lem1  40034  uhgr2edg  40435  domnmsuppn0  41944  mndpfsupp  41951  lincext3  42039