Theorem simpl2 1003

Description: Simplification rule. (Contributed by Jeff Hankins, 17-Nov-2009.)

Assertion

Ref	Expression
simpl2	⊢ (((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃) → 𝜓)

Proof of Theorem simpl2

Step	Hyp	Ref	Expression
1		simp2 1000	. 2 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜓)
2	1	adantr 276	1 ⊢ (((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃) → 𝜓)

Syntax hints:   → wi 4   ∧ wa 104   ∧ w3a 980

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107

This theorem depends on definitions:  df-bi 117  df-3an 982

This theorem is referenced by:  simpll2  1039  simprl2  1045  simp1l2  1093  simp2l2  1099  simp3l2  1105  3anandirs  1359  rspc3ev  2873  tfisi  4604  brcogw  4814  oawordi  6495  nnmord  6543  nnmword  6544  ac6sfi  6927  unsnfi  6948  unsnfidcel  6950  ordiso2  7065  prarloclemarch2  7449  enq0tr  7464  distrlem4prl  7614  distrlem4pru  7615  ltaprg  7649  aptiprlemu  7670  lelttr  8077  ltletr  8078  readdcan  8128  addcan  8168  addcan2  8169  ltadd2  8407  ltmul1a  8579  ltmul1  8580  divmulassap  8683  divmulasscomap  8684  lemul1a  8846  xrlelttr  9838  xrltletr  9839  xaddass  9901  xleadd1a  9905  xltadd1  9908  xlesubadd  9915  ixxdisj  9935  icoshftf1o  10023  icodisj  10024  lincmb01cmp  10035  iccf1o  10036  fztri3or  10071  ioom  10293  modqmuladdim  10400  modqmuladdnn0  10401  q2submod  10418  modqaddmulmod  10424  exp3val  10556  ltexp2a  10606  exple1  10610  expnbnd  10678  expnlbnd2  10680  nn0ltexp2  10724  nn0leexp2  10725  mulsubdivbinom2ap  10726  expcan  10731  fiprsshashgt1  10832  maxleastb  11258  maxltsup  11262  xrltmaxsup  11300  xrmaxltsup  11301  xrmaxaddlem  11303  xrmaxadd  11304  addcn2  11353  mulcn2  11355  geoisum1c  11563  dvdsval2  11832  dvdsmodexp  11837  dvdsadd2b  11882  dvdsaddre2b  11883  dvdsmod  11903  oexpneg  11917  divalglemex  11962  divalg  11964  gcdass  12051  rplpwr  12063  rppwr  12064  nnminle  12071  lcmass  12120  coprmdvds2  12128  rpmulgcd2  12130  rpdvds  12134  cncongr2  12139  rpexp  12188  znege1  12213  prmdiveq  12271  hashgcdlem  12273  odzdvds  12280  coprimeprodsq2  12293  pythagtriplem3  12302  pythagtriplem4  12303  pcdvdsb  12355  pcbc  12386  ctinf  12484  nninfdc  12507  isnsgrp  12884  issubmnd  12918  nmzsubg  13166  ghmnsgima  13224  srg1zr  13358  ring1eq0  13417  mulgass2  13427  rhmdvdsr  13542  rmodislmod  13684  topssnei  14139  cnptopco  14199  cnconst2  14210  cnptoprest  14216  cnpdis  14219  upxp  14249  bldisj  14378  blgt0  14379  bl2in  14380  blss2ps  14383  blss2  14384  xblm  14394  blssps  14404  blss  14405  xmetresbl  14417  bdbl  14480  bdmopn  14481  metcnp3  14488  metcnp  14489  metcnp2  14490  dvfvalap  14627  dvcnp2cntop  14640  dvcn  14641  logdivlti  14779  ltexp2  14837  lgsfvalg  14884  lgsneg  14903  lgsdilem  14906  lgsdirprm  14913  lgsdir  14914  lgsdi  14916  lgsne0  14917  1dom1el  15221