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  7306  offsplitfpar  8061  poseq  8100  omeulem2  8510  uniinqs  8734  unxpdomlem3  9158  elfiun  9333  cofsmo  10179  isfin2-2  10229  isf32lem9  10271  tskun  10697  tskurn  10700  reclem3pr  10960  dedekind  11296  subaddmulsub  11600  dmdcan  11851  lt2msq1  12026  supmullem1  12112  supmul  12114  xaddass2  13165  xlt2add  13175  xmulasslem3  13201  iccsplit  13401  expaddzlem  14028  expaddz  14029  expmulz  14031  limsupgle  15400  o1add  15537  o1mul  15538  o1sub  15539  bitsfzo  16362  sadfval  16379  smufval  16404  nn0rppwr  16488  prmexpb  16646  4sqlem18  16890  vdwlem10  16918  setsstruct2  17101  mrieqv2d  17562  curf1  18148  chnccat  18549  mgmsscl  18570  mndpfsupp  18692  mndodcong  19471  subgabl  19765  gex2abl  19780  ogrpinvlt  20073  cntzsubrng  20500  cntzsubr  20539  abvres  20764  lbsind2  21033  lbsextlem2  21114  lbsextg  21117  matring  22387  mdetunilem8  22563  maducoeval  22583  maducoeval2  22584  madurid  22588  cramerimplem3  22629  pmatcollpw2  22722  pm2mpf1  22743  cnprest  23233  isreg2  23321  fbssfi  23781  hausflimlem  23923  tmdgsum  24039  ssblps  24366  ssbl  24367  xrsmopn  24757  cphassi  25170  cphassir  25171  4cphipval2  25198  cphipval  25199  dvres2  25869  vieta1  26276  aalioulem4  26299  efgh  26506  cxpadd  26644  cxpsub  26647  divcxp  26652  cxple2  26662  cxplt2  26663  cxpcn3lem  26713  angcan  26768  ang180lem5  26779  isosctrlem3  26786  lgssq  27304  nosupinfsep  27700  noetalem1  27709  noeta2  27757  ltslpss  27904  bdayfinbndlem1  28463  brbtwn2  28978  axcontlem4  29040  axcontlem8  29044  uhgr2edg  29281  chscllem4  31715  cshwrnid  33043  pstmval  34052  measinblem  34377  cvmlift2lem6  35502  linethru  36347  cnres2  37960  lcv1  39297  lfl1  39326  lshpkrex  39374  hlrelat3  39668  cvrval3  39669  cvrval4N  39670  athgt  39712  atcvrlln2  39775  atcvrlln  39776  lvolnle3at  39838  lvolnlelpln  39841  4atlem11  39865  4atlem12  39868  2lplnj  39876  dalemddea  39940  cdlema2N  40048  paddasslem2  40077  atmod1i1m  40114  lhp2lt  40257  lhp0lt  40259  lhpexle3lem  40267  lhpj1  40278  lhpmcvr4N  40282  lhpelim  40293  lhpmod2i2  40294  lhpmod6i1  40295  cdlemb2  40297  lhpat  40299  ltrnatb  40393  ltrnel  40395  ltrncnvel  40398  ltrncnv  40402  trlval2  40419  trljat1  40422  trljat2  40423  trlnidatb  40433  cdlemc1  40447  cdlemc2  40448  cdlemc5  40451  cdlemc6  40452  cdleme0aa  40466  cdleme0b  40468  cdleme0c  40469  cdleme0e  40473  cdleme0fN  40474  cdleme01N  40477  cdleme0ex1N  40479  cdleme0moN  40481  cdleme3g  40490  cdleme3h  40491  cdleme3  40493  cdleme4  40494  cdleme4a  40495  cdleme5  40496  cdleme8  40506  cdleme9  40509  cdleme10  40510  cdleme16aN  40515  cdleme11fN  40520  cdleme11g  40521  cdleme11k  40524  cdleme13  40528  cdleme17c  40544  cdleme17d1  40545  cdleme18c  40549  cdleme22gb  40550  cdlemeda  40554  cdlemednpq  40555  cdlemednuN  40556  cdleme19c  40561  cdleme20aN  40565  cdleme20bN  40566  cdleme20c  40567  cdleme22aa  40595  cdleme22d  40599  cdleme22e  40600  cdleme27cl  40622  cdleme27a  40623  cdleme30a  40634  cdleme42a  40727  cdleme42c  40728  cdlemg2fv2  40856  cdlemg2m  40860  cdlemg4g  40872  cdlemg4  40873  cdlemg6c  40876  cdlemg7aN  40881  cdlemg9a  40888  cdlemg9b  40889  cdlemg10c  40895  cdlemg12a  40899  cdlemg12b  40900  cdlemg17a  40917  cdlemg18b  40935  cdlemg18c  40936  trlcoabs2N  40978  trlcolem  40982  tendoco2  41024  tendoicl  41052  cdlemi1  41074  cdlemi2  41075  cdlemj3  41079  tendocan  41080  cdlemk3  41089  cdlemk4  41090  cdlemk5a  41091  cdlemk9  41095  cdlemk9bN  41096  cdlemk10  41099  cdlemk30  41150  cdlemk31  41152  cdlemk39  41172  cdlemkfid1N  41177  cdlemkfid2N  41179  cdlemk19ylem  41186  cdlemk19xlem  41198  cdlemk53b  41212  cdlemk53  41213  cdlemk55a  41215  cdlemk43N  41219  cdlemk19u1  41225  cdlemm10N  41374  cdlemn2  41451  cdlemn10  41462  dihjustlem  41472  dihord2cN  41477  dihvalcq2  41503  dihopelvalcpre  41504  dihord5b  41515  dihord6b  41516  dihmeetlem2N  41555  dihmeetbclemN  41560  dihmeetlem4preN  41562  dihmeetALTN  41583  dochshpncl  41640  dochsatshpb  41708  hdmapval3N  42094  hgmap11  42158  f1o2d2  42485  remulcand  42690  pellfundex  43124  congtr  43203  fzmaxdif  43219  isnumbasgrplem2  43342  idomsubgmo  43431  ntrclsk13  44308  grumnudlem  44522  restuni3  45358  unirnmapsn  45454  ssmapsn  45456  infnsuprnmpt  45490  upbdrech  45549  suplesup  45580  infleinf  45612  supxrunb3  45639  mullimc  45858  islptre  45861  mullimcf  45865  neglimc  45887  limsupmnfuzlem  45966  limsupre3lem  45972  limsupre3uzlem  45975  icccncfext  46127  dvmptfprod  46185  stoweidlem31  46271  opnvonmbllem2  46873  smflimsuplem7  47066  ormkglobd  47115  funressneu  47289  cfsetsnfsetf1  47301  prmdvdsfmtnof1lem1  47826  uhgrimisgrgriclem  48172  clnbgrgrim  48176  grlimedgclnbgr  48237  domnmsuppn0  48611  lincext3  48698  2arymaptfo  48896