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

Syntax hints:   → wi 4   ∧ wa 395   ∧ 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 396  df-3an 1087

This theorem is referenced by:  simp11r  1283  simp21r  1289  simp31r  1295  eqfunresadj  7368  offsplitfpar  8124  poseq  8163  omeulem2  8604  uniinqs  8816  unxpdomlem3  9277  elfiun  9454  cofsmo  10293  isfin2-2  10343  isf32lem9  10385  tskun  10810  tskurn  10813  reclem3pr  11073  dedekind  11408  subaddmulsub  11708  dmdcan  11955  lt2msq1  12129  supmullem1  12215  supmul  12217  xaddass2  13262  xlt2add  13272  xmulasslem3  13298  iccsplit  13495  expaddzlem  14103  expaddz  14104  expmulz  14106  limsupgle  15454  o1add  15591  o1mul  15592  o1sub  15593  bitsfzo  16410  sadfval  16427  smufval  16452  prmexpb  16691  4sqlem18  16931  vdwlem10  16959  setsstruct2  17143  mrieqv2d  17619  curf1  18217  mgmsscl  18605  mndodcong  19497  subgabl  19791  gex2abl  19806  cntzsubrng  20504  cntzsubr  20545  abvres  20719  lbsind2  20966  lbsextlem2  21047  lbsextg  21050  matring  22358  mdetunilem8  22534  maducoeval  22554  maducoeval2  22555  madurid  22559  cramerimplem3  22600  pmatcollpw2  22693  pm2mpf1  22714  cnprest  23206  isreg2  23294  fbssfi  23754  hausflimlem  23896  tmdgsum  24012  ssblps  24341  ssbl  24342  xrsmopn  24741  cphassi  25155  cphassir  25156  4cphipval2  25183  cphipval  25184  dvres2  25854  vieta1  26260  aalioulem4  26283  efgh  26488  cxpadd  26626  cxpsub  26629  divcxp  26634  cxple2  26644  cxplt2  26645  cxpcn3lem  26695  angcan  26747  ang180lem5  26758  isosctrlem3  26765  lgssq  27283  nosupinfsep  27678  noetalem1  27687  noeta2  27730  sltlpss  27846  brbtwn2  28729  axcontlem4  28791  axcontlem8  28795  uhgr2edg  29034  chscllem4  31463  cshwrnid  32695  ogrpinvlt  32816  pstmval  33496  measinblem  33839  cvmlift2lem6  34918  linethru  35749  cnres2  37236  lcv1  38513  lfl1  38542  lshpkrex  38590  hlrelat3  38885  cvrval3  38886  cvrval4N  38887  athgt  38929  atcvrlln2  38992  atcvrlln  38993  lvolnle3at  39055  lvolnlelpln  39058  4atlem11  39082  4atlem12  39085  2lplnj  39093  dalemddea  39157  cdlema2N  39265  paddasslem2  39294  atmod1i1m  39331  lhp2lt  39474  lhp0lt  39476  lhpexle3lem  39484  lhpj1  39495  lhpmcvr4N  39499  lhpelim  39510  lhpmod2i2  39511  lhpmod6i1  39512  cdlemb2  39514  lhpat  39516  ltrnatb  39610  ltrnel  39612  ltrncnvel  39615  ltrncnv  39619  trlval2  39636  trljat1  39639  trljat2  39640  trlnidatb  39650  cdlemc1  39664  cdlemc2  39665  cdlemc5  39668  cdlemc6  39669  cdleme0aa  39683  cdleme0b  39685  cdleme0c  39686  cdleme0e  39690  cdleme0fN  39691  cdleme01N  39694  cdleme0ex1N  39696  cdleme0moN  39698  cdleme3g  39707  cdleme3h  39708  cdleme3  39710  cdleme4  39711  cdleme4a  39712  cdleme5  39713  cdleme8  39723  cdleme9  39726  cdleme10  39727  cdleme16aN  39732  cdleme11fN  39737  cdleme11g  39738  cdleme11k  39741  cdleme13  39745  cdleme17c  39761  cdleme17d1  39762  cdleme18c  39766  cdleme22gb  39767  cdlemeda  39771  cdlemednpq  39772  cdlemednuN  39773  cdleme19c  39778  cdleme20aN  39782  cdleme20bN  39783  cdleme20c  39784  cdleme22aa  39812  cdleme22d  39816  cdleme22e  39817  cdleme27cl  39839  cdleme27a  39840  cdleme30a  39851  cdleme42a  39944  cdleme42c  39945  cdlemg2fv2  40073  cdlemg2m  40077  cdlemg4g  40089  cdlemg4  40090  cdlemg6c  40093  cdlemg7aN  40098  cdlemg9a  40105  cdlemg9b  40106  cdlemg10c  40112  cdlemg12a  40116  cdlemg12b  40117  cdlemg17a  40134  cdlemg18b  40152  cdlemg18c  40153  trlcoabs2N  40195  trlcolem  40199  tendoco2  40241  tendoicl  40269  cdlemi1  40291  cdlemi2  40292  cdlemj3  40296  tendocan  40297  cdlemk3  40306  cdlemk4  40307  cdlemk5a  40308  cdlemk9  40312  cdlemk9bN  40313  cdlemk10  40316  cdlemk30  40367  cdlemk31  40369  cdlemk39  40389  cdlemkfid1N  40394  cdlemkfid2N  40396  cdlemk19ylem  40403  cdlemk19xlem  40415  cdlemk53b  40429  cdlemk53  40430  cdlemk55a  40432  cdlemk43N  40436  cdlemk19u1  40442  cdlemm10N  40591  cdlemn2  40668  cdlemn10  40679  dihjustlem  40689  dihord2cN  40694  dihvalcq2  40720  dihopelvalcpre  40721  dihord5b  40732  dihord6b  40733  dihmeetlem2N  40772  dihmeetbclemN  40777  dihmeetlem4preN  40779  dihmeetALTN  40800  dochshpncl  40857  dochsatshpb  40925  hdmapval3N  41311  hgmap11  41375  f1o2d2  41724  nn0rppwr  41893  remulcand  41993  pellfundex  42306  congtr  42386  fzmaxdif  42402  isnumbasgrplem2  42528  idomsubgmo  42621  ntrclsk13  43501  grumnudlem  43722  restuni3  44484  unirnmapsn  44587  ssmapsn  44589  infnsuprnmpt  44626  upbdrech  44687  suplesup  44721  infleinf  44754  supxrunb3  44781  mullimc  45004  islptre  45007  mullimcf  45011  neglimc  45035  limsupmnfuzlem  45114  limsupre3lem  45120  limsupre3uzlem  45123  icccncfext  45275  dvmptfprod  45333  stoweidlem31  45419  opnvonmbllem2  46021  smflimsuplem7  46214  funressneu  46429  cfsetsnfsetf1  46441  prmdvdsfmtnof1lem1  46924  domnmsuppn0  47433  mndpfsupp  47440  lincext3  47524  2arymaptfo  47727