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  7371  offsplitfpar  8123  mpof1o2d  8130  poseq  8163  omeulem2  8577  uniinqs  8804  unxpdomlem3  9228  elfiun  9400  cofsmo  10271  isfin2-2  10321  isf32lem9  10363  tskun  10789  tskurn  10792  reclem3pr  11052  dedekind  11391  subaddmulsub  11695  dmdcan  11943  lt2msq1  12117  supmullem1  12203  supmul  12205  xaddass2  13294  xlt2add  13304  xmulasslem3  13330  iccsplit  13530  expaddzlem  14161  expaddz  14162  expmulz  14164  limsupgle  15554  o1add  15691  o1mul  15692  o1sub  15693  bitsfzo  16518  sadfval  16535  smufval  16560  nn0rppwr  16644  prmexpb  16803  4sqlem18  17047  vdwlem10  17075  setsstruct2  17259  mrieqv2d  17720  curf1  18306  chnccat  18707  mgmsscl  18728  mndpfsupp  18856  mndodcong  19643  subgabl  19937  gex2abl  19952  ogrpinvlt  20245  rng1zrlem  20290  cntzsubrng  20703  cntzsubr  20742  abvres  20971  lbsind2  21239  lbsextlem2  21320  lbsextg  21323  matring  22637  mdetunilem8  22813  maducoeval  22833  maducoeval2  22834  madurid  22838  cramerimplem3  22879  pmatcollpw2  22972  pm2mpf1  22993  cnprest  23483  isreg2  23571  fbssfi  24031  hausflimlem  24173  tmdgsum  24289  ssblps  24616  ssbl  24617  xrsmopn  25007  cphassi  25410  cphassir  25411  4cphipval2  25438  cphipval  25439  dvres2  26108  vieta1  26510  aalioulem4  26535  efgh  26743  cxpadd  26881  cxpsub  26884  divcxp  26889  cxple2  26899  cxplt2  26900  cxpcn3lem  26949  angcan  27004  ang180lem5  27015  isosctrlem3  27022  lgssq  27538  nosupinfsep  27933  noetalem1  27942  noeta2  27991  ltslpss  28138  bdayfinbndlem1  28697  brbtwn2  29292  axcontlem4  29354  axcontlem8  29358  uhgr2edg  29595  chscllem4  32029  cshwrnid  33312  pstmval  34316  measinblem  34642  cvmlift2lem6  35821  linethru  36666  cnres2  38455  lcv1  39856  lfl1  39885  lshpkrex  39933  hlrelat3  40227  cvrval3  40228  cvrval4N  40229  athgt  40271  atcvrlln2  40334  atcvrlln  40335  lvolnle3at  40397  lvolnlelpln  40400  4atlem11  40424  4atlem12  40427  2lplnj  40435  dalemddea  40499  cdlema2N  40607  paddasslem2  40636  atmod1i1m  40673  lhp2lt  40816  lhp0lt  40818  lhpexle3lem  40826  lhpj1  40837  lhpmcvr4N  40841  lhpelim  40852  lhpmod2i2  40853  lhpmod6i1  40854  cdlemb2  40856  lhpat  40858  ltrnatb  40952  ltrnel  40954  ltrncnvel  40957  ltrncnv  40961  trlval2  40978  trljat1  40981  trljat2  40982  trlnidatb  40992  cdlemc1  41006  cdlemc2  41007  cdlemc5  41010  cdlemc6  41011  cdleme0aa  41025  cdleme0b  41027  cdleme0c  41028  cdleme0e  41032  cdleme0fN  41033  cdleme01N  41036  cdleme0ex1N  41038  cdleme0moN  41040  cdleme3g  41049  cdleme3h  41050  cdleme3  41052  cdleme4  41053  cdleme4a  41054  cdleme5  41055  cdleme8  41065  cdleme9  41068  cdleme10  41069  cdleme16aN  41074  cdleme11fN  41079  cdleme11g  41080  cdleme11k  41083  cdleme13  41087  cdleme17c  41103  cdleme17d1  41104  cdleme18c  41108  cdleme22gb  41109  cdlemeda  41113  cdlemednpq  41114  cdlemednuN  41115  cdleme19c  41120  cdleme20aN  41124  cdleme20bN  41125  cdleme20c  41126  cdleme22aa  41154  cdleme22d  41158  cdleme22e  41159  cdleme27cl  41181  cdleme27a  41182  cdleme30a  41193  cdleme42a  41286  cdleme42c  41287  cdlemg2fv2  41415  cdlemg2m  41419  cdlemg4g  41431  cdlemg4  41432  cdlemg6c  41435  cdlemg7aN  41440  cdlemg9a  41447  cdlemg9b  41448  cdlemg10c  41454  cdlemg12a  41458  cdlemg12b  41459  cdlemg17a  41476  cdlemg18b  41494  cdlemg18c  41495  trlcoabs2N  41537  trlcolem  41541  tendoco2  41583  tendoicl  41611  cdlemi1  41633  cdlemi2  41634  cdlemj3  41638  tendocan  41639  cdlemk3  41648  cdlemk4  41649  cdlemk5a  41650  cdlemk9  41654  cdlemk9bN  41655  cdlemk10  41658  cdlemk30  41709  cdlemk31  41711  cdlemk39  41731  cdlemkfid1N  41736  cdlemkfid2N  41738  cdlemk19ylem  41745  cdlemk19xlem  41757  cdlemk53b  41771  cdlemk53  41772  cdlemk55a  41774  cdlemk43N  41778  cdlemk19u1  41784  cdlemm10N  41933  cdlemn2  42010  cdlemn10  42021  dihjustlem  42031  dihord2cN  42036  dihvalcq2  42062  dihopelvalcpre  42063  dihord5b  42074  dihord6b  42075  dihmeetlem2N  42114  dihmeetbclemN  42119  dihmeetlem4preN  42121  dihmeetALTN  42142  dochshpncl  42199  dochsatshpb  42267  hdmapval3N  42653  hgmap11  42717  remulcand  43241  pellfundex  43654  congtr  43733  fzmaxdif  43749  isnumbasgrplem2  43872  idomsubgmo  43961  ntrclsk13  44838  grumnudlem  45036  restuni3  45877  unirnmapsn  45971  ssmapsn  45973  infnsuprnmpt  46006  upbdrech  46065  suplesup  46096  infleinf  46128  supxrunb3  46155  mullimc  46373  islptre  46376  mullimcf  46380  neglimc  46402  limsupmnfuzlem  46481  limsupre3lem  46487  limsupre3uzlem  46490  icccncfext  46642  dvmptfprod  46700  stoweidlem31  46786  opnvonmbllem2  47388  smflimsuplem7  47581  ormkglobd  47632  funressneu  47825  cfsetsnfsetf1  47837  prmdvdsfmtnof1lem1  48377  uhgrimisgrgriclem  48736  clnbgrgrim  48740  grlimedgclnbgr  48801  domnmsuppn0  49190  lincext3  49277  2arymaptfo  49475