Theorem simp1r 1198

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 1087

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 1089

This theorem is referenced by:  simp11r  1285  simp21r  1291  simp31r  1297  eqfunresadj  7396  offsplitfpar  8160  poseq  8199  omeulem2  8639  uniinqs  8855  unxpdomlem3  9315  elfiun  9499  cofsmo  10338  isfin2-2  10388  isf32lem9  10430  tskun  10855  tskurn  10858  reclem3pr  11118  dedekind  11453  subaddmulsub  11753  dmdcan  12004  lt2msq1  12179  supmullem1  12265  supmul  12267  xaddass2  13312  xlt2add  13322  xmulasslem3  13348  iccsplit  13545  expaddzlem  14156  expaddz  14157  expmulz  14159  limsupgle  15523  o1add  15660  o1mul  15661  o1sub  15662  bitsfzo  16481  sadfval  16498  smufval  16523  nn0rppwr  16608  prmexpb  16766  4sqlem18  17009  vdwlem10  17037  setsstruct2  17221  mrieqv2d  17697  curf1  18295  mgmsscl  18683  mndodcong  19584  subgabl  19878  gex2abl  19893  cntzsubrng  20593  cntzsubr  20634  abvres  20854  lbsind2  21103  lbsextlem2  21184  lbsextg  21187  matring  22470  mdetunilem8  22646  maducoeval  22666  maducoeval2  22667  madurid  22671  cramerimplem3  22712  pmatcollpw2  22805  pm2mpf1  22826  cnprest  23318  isreg2  23406  fbssfi  23866  hausflimlem  24008  tmdgsum  24124  ssblps  24453  ssbl  24454  xrsmopn  24853  cphassi  25267  cphassir  25268  4cphipval2  25295  cphipval  25296  dvres2  25967  vieta1  26372  aalioulem4  26395  efgh  26601  cxpadd  26739  cxpsub  26742  divcxp  26747  cxple2  26757  cxplt2  26758  cxpcn3lem  26808  angcan  26863  ang180lem5  26874  isosctrlem3  26881  lgssq  27399  nosupinfsep  27795  noetalem1  27804  noeta2  27847  sltlpss  27963  brbtwn2  28938  axcontlem4  29000  axcontlem8  29004  uhgr2edg  29243  chscllem4  31672  cshwrnid  32928  ogrpinvlt  33073  pstmval  33841  measinblem  34184  cvmlift2lem6  35276  linethru  36117  cnres2  37723  lcv1  38997  lfl1  39026  lshpkrex  39074  hlrelat3  39369  cvrval3  39370  cvrval4N  39371  athgt  39413  atcvrlln2  39476  atcvrlln  39477  lvolnle3at  39539  lvolnlelpln  39542  4atlem11  39566  4atlem12  39569  2lplnj  39577  dalemddea  39641  cdlema2N  39749  paddasslem2  39778  atmod1i1m  39815  lhp2lt  39958  lhp0lt  39960  lhpexle3lem  39968  lhpj1  39979  lhpmcvr4N  39983  lhpelim  39994  lhpmod2i2  39995  lhpmod6i1  39996  cdlemb2  39998  lhpat  40000  ltrnatb  40094  ltrnel  40096  ltrncnvel  40099  ltrncnv  40103  trlval2  40120  trljat1  40123  trljat2  40124  trlnidatb  40134  cdlemc1  40148  cdlemc2  40149  cdlemc5  40152  cdlemc6  40153  cdleme0aa  40167  cdleme0b  40169  cdleme0c  40170  cdleme0e  40174  cdleme0fN  40175  cdleme01N  40178  cdleme0ex1N  40180  cdleme0moN  40182  cdleme3g  40191  cdleme3h  40192  cdleme3  40194  cdleme4  40195  cdleme4a  40196  cdleme5  40197  cdleme8  40207  cdleme9  40210  cdleme10  40211  cdleme16aN  40216  cdleme11fN  40221  cdleme11g  40222  cdleme11k  40225  cdleme13  40229  cdleme17c  40245  cdleme17d1  40246  cdleme18c  40250  cdleme22gb  40251  cdlemeda  40255  cdlemednpq  40256  cdlemednuN  40257  cdleme19c  40262  cdleme20aN  40266  cdleme20bN  40267  cdleme20c  40268  cdleme22aa  40296  cdleme22d  40300  cdleme22e  40301  cdleme27cl  40323  cdleme27a  40324  cdleme30a  40335  cdleme42a  40428  cdleme42c  40429  cdlemg2fv2  40557  cdlemg2m  40561  cdlemg4g  40573  cdlemg4  40574  cdlemg6c  40577  cdlemg7aN  40582  cdlemg9a  40589  cdlemg9b  40590  cdlemg10c  40596  cdlemg12a  40600  cdlemg12b  40601  cdlemg17a  40618  cdlemg18b  40636  cdlemg18c  40637  trlcoabs2N  40679  trlcolem  40683  tendoco2  40725  tendoicl  40753  cdlemi1  40775  cdlemi2  40776  cdlemj3  40780  tendocan  40781  cdlemk3  40790  cdlemk4  40791  cdlemk5a  40792  cdlemk9  40796  cdlemk9bN  40797  cdlemk10  40800  cdlemk30  40851  cdlemk31  40853  cdlemk39  40873  cdlemkfid1N  40878  cdlemkfid2N  40880  cdlemk19ylem  40887  cdlemk19xlem  40899  cdlemk53b  40913  cdlemk53  40914  cdlemk55a  40916  cdlemk43N  40920  cdlemk19u1  40926  cdlemm10N  41075  cdlemn2  41152  cdlemn10  41163  dihjustlem  41173  dihord2cN  41178  dihvalcq2  41204  dihopelvalcpre  41205  dihord5b  41216  dihord6b  41217  dihmeetlem2N  41256  dihmeetbclemN  41261  dihmeetlem4preN  41263  dihmeetALTN  41284  dochshpncl  41341  dochsatshpb  41409  hdmapval3N  41795  hgmap11  41859  f1o2d2  42228  remulcand  42414  pellfundex  42842  congtr  42922  fzmaxdif  42938  isnumbasgrplem2  43061  idomsubgmo  43154  ntrclsk13  44033  grumnudlem  44254  restuni3  45020  unirnmapsn  45121  ssmapsn  45123  infnsuprnmpt  45159  upbdrech  45220  suplesup  45254  infleinf  45287  supxrunb3  45314  mullimc  45537  islptre  45540  mullimcf  45544  neglimc  45568  limsupmnfuzlem  45647  limsupre3lem  45653  limsupre3uzlem  45656  icccncfext  45808  dvmptfprod  45866  stoweidlem31  45952  opnvonmbllem2  46554  smflimsuplem7  46747  funressneu  46962  cfsetsnfsetf1  46974  prmdvdsfmtnof1lem1  47458  uhgrimisgrgriclem  47782  clnbgrgrim  47786  domnmsuppn0  48094  mndpfsupp  48101  lincext3  48185  2arymaptfo  48388