Theorem simp1r 1086

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

Syntax hints:   → wi 4   ∧ wa 384   ∧ w3a 1037

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 197  df-an 386  df-3an 1039

This theorem is referenced by:  simpl1r  1113  simpr1r  1119  simp11r  1173  simp21r  1179  simp31r  1185  vtoclgftOLD  3255  funprgOLD  5941  omeulem2  7663  uniinqs  7827  unxpdomlem3  8166  elfiun  8336  cofsmo  9091  isfin2-2  9141  isf32lem9  9183  tskun  9608  tskurn  9611  reclem3pr  9871  dedekind  10200  dmdcan  10735  lt2msq1  10907  supmullem1  10993  supmul  10995  xaddass2  12080  xlt2add  12090  xmulasslem3  12116  iccsplit  12305  expaddzlem  12903  expaddz  12904  expmulz  12906  limsupgle  14208  o1add  14344  o1mul  14345  o1sub  14346  bitsfzo  15157  sadfval  15174  smufval  15199  prmexpb  15430  4sqlem18  15666  vdwlem10  15694  setsstruct2  15896  mrieqv2d  16299  curf1  16865  mndodcong  17961  subgabl  18241  gex2abl  18254  cntzsubr  18812  abvres  18839  lbsind2  19081  lbsextlem2  19159  lbsextg  19162  matring  20249  mdetunilem8  20425  maducoeval  20445  maducoeval2  20446  madurid  20450  cramerimplem3  20491  pmatcollpw2  20583  pm2mpf1  20604  cnprest  21093  isreg2  21181  fbssfi  21641  hausflimlem  21783  tmdgsum  21899  ssblps  22227  ssbl  22228  xrsmopn  22615  cphassi  23014  cphassir  23015  4cphipval2  23041  cphipval  23042  dvres2  23676  vieta1  24067  aalioulem4  24090  efgh  24287  cxpadd  24425  cxpsub  24428  divcxp  24433  cxple2  24443  cxplt2  24444  cxpcn3lem  24488  angcan  24532  ang180lem5  24543  isosctrlem3  24550  lgssq  25062  brbtwn2  25785  axcontlem4  25847  axcontlem8  25851  uhgr2edg  26100  chscllem4  28499  ogrpinvlt  29724  pstmval  29938  measinblem  30283  cvmlift2lem6  31290  eqfunresadj  31659  poseq  31750  noetalem5  31867  linethru  32260  cnres2  33562  lcv1  34328  lfl1  34357  lshpkrex  34405  hlrelat3  34698  cvrval3  34699  cvrval4N  34700  athgt  34742  atcvrlln2  34805  atcvrlln  34806  lvolnle3at  34868  lvolnlelpln  34871  4atlem11  34895  4atlem12  34898  2lplnj  34906  dalemddea  34970  cdlema2N  35078  paddasslem2  35107  atmod1i1m  35144  lhp2lt  35287  lhp0lt  35289  lhpexle3lem  35297  lhpj1  35308  lhpmcvr4N  35312  lhpelim  35323  lhpmod2i2  35324  lhpmod6i1  35325  cdlemb2  35327  lhpat  35329  ltrnatb  35423  ltrnel  35425  ltrncnvel  35428  ltrncnv  35432  ltrnmwOLD  35438  trlval2  35450  trljat1  35453  trljat2  35454  trlnidatb  35464  cdlemc1  35478  cdlemc2  35479  cdlemc5  35482  cdlemc6  35483  cdleme0aa  35497  cdleme0b  35499  cdleme0c  35500  cdleme0e  35504  cdleme0fN  35505  cdleme01N  35508  cdleme0ex1N  35510  cdleme0moN  35512  cdleme3g  35521  cdleme3h  35522  cdleme3  35524  cdleme4  35525  cdleme4a  35526  cdleme5  35527  cdleme8  35537  cdleme9  35540  cdleme10  35541  cdleme16aN  35546  cdleme11fN  35551  cdleme11g  35552  cdleme11k  35555  cdleme13  35559  cdleme17c  35575  cdleme17d1  35576  cdleme18c  35580  cdleme22gb  35581  cdlemeda  35585  cdlemednpq  35586  cdlemednuN  35587  cdleme19c  35593  cdleme20aN  35597  cdleme20bN  35598  cdleme20c  35599  cdleme22aa  35627  cdleme22d  35631  cdleme22e  35632  cdleme27cl  35654  cdleme27a  35655  cdleme30a  35666  cdleme42a  35759  cdleme42c  35760  cdlemg2fv2  35888  cdlemg2m  35892  cdlemg4g  35904  cdlemg4  35905  cdlemg6c  35908  cdlemg7aN  35913  cdlemg9a  35920  cdlemg9b  35921  cdlemg10c  35927  cdlemg12a  35931  cdlemg12b  35932  cdlemg17a  35949  cdlemg18b  35967  cdlemg18c  35968  trlcoabs2N  36010  trlcolem  36014  tendoco2  36056  tendoicl  36084  cdlemi1  36106  cdlemi2  36107  cdlemj3  36111  tendocan  36112  cdlemk3  36121  cdlemk4  36122  cdlemk5a  36123  cdlemk9  36127  cdlemk9bN  36128  cdlemk10  36131  cdlemk30  36182  cdlemk31  36184  cdlemk39  36204  cdlemkfid1N  36209  cdlemkfid2N  36211  cdlemk19ylem  36218  cdlemk19xlem  36230  cdlemk53b  36244  cdlemk53  36245  cdlemk55a  36247  cdlemk43N  36251  cdlemk19u1  36257  cdlemm10N  36407  cdlemn2  36484  cdlemn10  36495  dihjustlem  36505  dihord2cN  36510  dihvalcq2  36536  dihopelvalcpre  36537  dihord5b  36548  dihord6b  36549  dihmeetlem2N  36588  dihmeetbclemN  36593  dihmeetlem4preN  36595  dihmeetALTN  36616  dochshpncl  36673  dochsatshpb  36741  hdmapval3N  37130  hgmap11  37194  pellfundex  37450  congtr  37532  fzmaxdif  37548  isnumbasgrplem2  37674  idomsubgmo  37776  ntrclsk13  38369  restuni3  39301  unirnmapsn  39406  ssmapsn  39408  infnsuprnmpt  39465  upbdrech  39519  suplesup  39555  infleinf  39588  supxrunb3  39623  mullimc  39848  islptre  39851  mullimcf  39855  neglimc  39879  limsupmnfuzlem  39958  limsupre3lem  39964  limsupre3uzlem  39967  icccncfext  40100  dvmptfprod  40160  stoweidlem31  40248  opnvonmbllem2  40847  smflimsuplem7  41032  prmdvdsfmtnof1lem1  41496  domnmsuppn0  42150  mndpfsupp  42157  lincext3  42245