Theorem simpl2 950

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

Assertion

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

Proof of Theorem simpl2

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

Syntax hints:   → wi 4   ∧ wa 103   ∧ w3a 927

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

This theorem depends on definitions:  df-bi 116  df-3an 929

This theorem is referenced by:  simpll2  986  simprl2  992  simp1l2  1040  simp2l2  1046  simp3l2  1052  3anandirs  1291  rspc3ev  2752  tfisi  4430  brcogw  4636  oawordi  6270  nnmord  6316  nnmword  6317  ac6sfi  6694  unsnfi  6709  unsnfidcel  6711  ordiso2  6808  prarloclemarch2  7075  enq0tr  7090  distrlem4prl  7240  distrlem4pru  7241  ltaprg  7275  aptiprlemu  7296  lelttr  7670  ltletr  7671  readdcan  7719  addcan  7759  addcan2  7760  ltadd2  7994  ltmul1a  8165  ltmul1  8166  divmulassap  8259  divmulasscomap  8260  lemul1a  8416  xrlelttr  9372  xrltletr  9373  xaddass  9435  xleadd1a  9439  xltadd1  9442  xlesubadd  9449  ixxdisj  9469  icoshftf1o  9557  icodisj  9558  lincmb01cmp  9569  iccf1o  9570  fztri3or  9602  ioom  9821  modqmuladdim  9923  modqmuladdnn0  9924  q2submod  9941  modqaddmulmod  9947  exp3val  10088  ltexp2a  10138  exple1  10142  expnbnd  10208  expnlbnd2  10210  expcan  10256  fiprsshashgt1  10356  maxleastb  10778  maxltsup  10782  xrltmaxsup  10816  xrmaxltsup  10817  xrmaxaddlem  10819  xrmaxadd  10820  addcn2  10869  mulcn2  10871  geoisum1c  11078  dvdsval2  11241  dvdsadd2b  11285  dvdsmod  11305  oexpneg  11319  divalglemex  11364  divalg  11366  gcdass  11446  rplpwr  11458  rppwr  11459  lcmass  11509  coprmdvds2  11517  rpmulgcd2  11519  rpdvds  11523  cncongr2  11528  rpexp  11574  znege1  11598  hashgcdlem  11645  topssnei  12029  cnptopco  12088  cnconst2  12099  cnptoprest  12105  cnpdis  12108  bldisj  12202  blgt0  12203  bl2in  12204  blss2ps  12207  blss2  12208  xblm  12218  blssps  12228  blss  12229  xmetresbl  12241  bdbl  12304  bdmopn  12305  metcnp3  12308  metcnp  12309  metcnp2  12310