Theorem simp1r 1217

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∧ w3a 1103

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105

This theorem is used by:  simp11r  1304  simp21r  1310  simp31r  1316  eqfunresadj  7370  offsplitfpar  8132  mpof1o2d  8139  poseq  8177  omeulem2  8594  uniinqs  8821  unxpdomlem3  9252  elfiun  9425  cofsmo  10350  isfin2-2  10400  isf32lem9  10442  tskun  10874  tskurn  10877  reclem3pr  11137  dedekind  11476  subaddmulsub  11782  dmdcan  12030  lt2msq1  12204  supmullem1  12290  supmul  12292  xaddass2  13383  xlt2add  13393  xmulasslem3  13419  iccsplit  13619  expaddzlem  14251  expaddz  14252  expmulz  14254  limsupgle  15649  o1add  15786  o1mul  15787  o1sub  15788  bitsfzo  16610  sadfval  16627  smufval  16652  nn0rppwr  16740  prmexpb  16900  4sqlem18  17145  vdwlem10  17173  setsstruct2  17357  mrieqv2d  17818  curf1  18404  chnccat  18805  mgmsscl  18826  mndpfsupp  18966  mndodcong  19761  subgabl  20055  gex2abl  20070  ogrpinvlt  20363  rng1zrlem  20408  cntzsubrng  20824  cntzsubr  20863  abvres  21093  lbsind2  21361  lbsextlem2  21442  lbsextg  21445  matring  22763  mdetunilem8  22939  maducoeval  22959  maducoeval2  22960  madurid  22964  cramerimplem3  23008  pmatcollpw2  23101  pm2mpf1  23122  cnprest  23612  isreg2  23700  fbssfi  24161  hausflimlem  24303  tmdgsum  24419  ssblps  24746  ssbl  24747  xrsmopn  25137  cphassi  25540  cphassir  25541  4cphipval2  25568  cphipval  25569  dvres2  26237  vieta1  26640  aalioulem4  26667  efgh  26874  cxpadd  27012  cxpsub  27015  divcxp  27020  cxple2  27030  cxplt2  27031  cxpcn3lem  27080  angcan  27135  ang180lem5  27146  isosctrlem3  27153  lgssq  27669  nosupinfsep  28094  noetalem1  28103  noeta2  28152  ltslpss  28299  bdayfinbndlem1  28858  brbtwn2  29488  axcontlem4  29550  axcontlem8  29554  uhgr2edg  29794  chscllem4  32247  cshwrnid  33568  pstmval  34573  measinblem  34899  cvmlift2lem6  36159  linethru  37010  cnres2  38790  lcv1  40191  lfl1  40220  lshpkrex  40268  hlrelat3  40562  cvrval3  40563  cvrval4N  40564  athgt  40606  atcvrlln2  40669  atcvrlln  40670  lvolnle3at  40732  lvolnlelpln  40735  4atlem11  40759  4atlem12  40762  2lplnj  40770  dalemddea  40834  cdlema2N  40942  paddasslem2  40971  atmod1i1m  41008  lhp2lt  41151  lhp0lt  41153  lhpexle3lem  41161  lhpj1  41172  lhpmcvr4N  41176  lhpelim  41187  lhpmod2i2  41188  lhpmod6i1  41189  cdlemb2  41191  lhpat  41193  ltrnatb  41287  ltrnel  41289  ltrncnvel  41292  ltrncnv  41296  trlval2  41313  trljat1  41316  trljat2  41317  trlnidatb  41327  cdlemc1  41341  cdlemc2  41342  cdlemc5  41345  cdlemc6  41346  cdleme0aa  41360  cdleme0b  41362  cdleme0c  41363  cdleme0e  41367  cdleme0fN  41368  cdleme01N  41371  cdleme0ex1N  41373  cdleme0moN  41375  cdleme3g  41384  cdleme3h  41385  cdleme3  41387  cdleme4  41388  cdleme4a  41389  cdleme5  41390  cdleme8  41400  cdleme9  41403  cdleme10  41404  cdleme16aN  41409  cdleme11fN  41414  cdleme11g  41415  cdleme11k  41418  cdleme13  41422  cdleme17c  41438  cdleme17d1  41439  cdleme18c  41443  cdleme22gb  41444  cdlemeda  41448  cdlemednpq  41449  cdlemednuN  41450  cdleme19c  41455  cdleme20aN  41459  cdleme20bN  41460  cdleme20c  41461  cdleme22aa  41489  cdleme22d  41493  cdleme22e  41494  cdleme27cl  41516  cdleme27a  41517  cdleme30a  41528  cdleme42a  41621  cdleme42c  41622  cdlemg2fv2  41750  cdlemg2m  41754  cdlemg4g  41766  cdlemg4  41767  cdlemg6c  41770  cdlemg7aN  41775  cdlemg9a  41782  cdlemg9b  41783  cdlemg10c  41789  cdlemg12a  41793  cdlemg12b  41794  cdlemg17a  41811  cdlemg18b  41829  cdlemg18c  41830  trlcoabs2N  41872  trlcolem  41876  tendoco2  41918  tendoicl  41946  cdlemi1  41968  cdlemi2  41969  cdlemj3  41973  tendocan  41974  cdlemk3  41983  cdlemk4  41984  cdlemk5a  41985  cdlemk9  41989  cdlemk9bN  41990  cdlemk10  41993  cdlemk30  42044  cdlemk31  42046  cdlemk39  42066  cdlemkfid1N  42071  cdlemkfid2N  42073  cdlemk19ylem  42080  cdlemk19xlem  42092  cdlemk53b  42106  cdlemk53  42107  cdlemk55a  42109  cdlemk43N  42113  cdlemk19u1  42119  cdlemm10N  42268  cdlemn2  42345  cdlemn10  42356  dihjustlem  42366  dihord2cN  42371  dihvalcq2  42397  dihopelvalcpre  42398  dihord5b  42409  dihord6b  42410  dihmeetlem2N  42449  dihmeetbclemN  42454  dihmeetlem4preN  42456  dihmeetALTN  42477  dochshpncl  42534  dochsatshpb  42602  hdmapval3N  42988  hgmap11  43052  remulcand  43583  pellfundex  43986  congtr  44065  fzmaxdif  44081  isnumbasgrplem2  44199  idomsubgmo  44288  ntrclsk13  45164  grumnudlem  45362  restuni3  46226  unirnmapsn  46320  ssmapsn  46322  infnsuprnmpt  46355  upbdrech  46414  suplesup  46444  infleinf  46476  supxrunb3  46503  mullimc  46721  islptre  46724  mullimcf  46728  neglimc  46750  limsupmnfuzlem  46829  limsupre3lem  46835  limsupre3uzlem  46838  icccncfext  46990  dvmptfprod  47048  stoweidlem31  47134  opnvonmbllem2  47736  smflimsuplem7  47929  ormkglobd  47980  funressneu  48210  cfsetsnfsetf1  48222  prmdvdsfmtnof1lem1  48762  uhgrimisgrgriclem  49121  clnbgrgrim  49125  grlimedgclnbgr  49186  domnmsuppn0  49574  lincext3  49661  2arymaptfo  49859