Theorem simpl2 986

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

Assertion

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

Proof of Theorem simpl2

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

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

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

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

This theorem is referenced by:  simpll2  1022  simprl2  1028  simp1l2  1076  simp2l2  1082  simp3l2  1088  3anandirs  1327  rspc3ev  2810  tfisi  4509  brcogw  4716  oawordi  6373  nnmord  6421  nnmword  6422  ac6sfi  6800  unsnfi  6815  unsnfidcel  6817  ordiso2  6928  prarloclemarch2  7251  enq0tr  7266  distrlem4prl  7416  distrlem4pru  7417  ltaprg  7451  aptiprlemu  7472  lelttr  7876  ltletr  7877  readdcan  7926  addcan  7966  addcan2  7967  ltadd2  8205  ltmul1a  8377  ltmul1  8378  divmulassap  8479  divmulasscomap  8480  lemul1a  8640  xrlelttr  9619  xrltletr  9620  xaddass  9682  xleadd1a  9686  xltadd1  9689  xlesubadd  9696  ixxdisj  9716  icoshftf1o  9804  icodisj  9805  lincmb01cmp  9816  iccf1o  9817  fztri3or  9850  ioom  10069  modqmuladdim  10171  modqmuladdnn0  10172  q2submod  10189  modqaddmulmod  10195  exp3val  10326  ltexp2a  10376  exple1  10380  expnbnd  10446  expnlbnd2  10448  expcan  10494  fiprsshashgt1  10595  maxleastb  11018  maxltsup  11022  xrltmaxsup  11058  xrmaxltsup  11059  xrmaxaddlem  11061  xrmaxadd  11062  addcn2  11111  mulcn2  11113  geoisum1c  11321  dvdsval2  11532  dvdsadd2b  11576  dvdsmod  11596  oexpneg  11610  divalglemex  11655  divalg  11657  gcdass  11739  rplpwr  11751  rppwr  11752  lcmass  11802  coprmdvds2  11810  rpmulgcd2  11812  rpdvds  11816  cncongr2  11821  rpexp  11867  znege1  11892  hashgcdlem  11939  ctinf  11979  topssnei  12370  cnptopco  12430  cnconst2  12441  cnptoprest  12447  cnpdis  12450  upxp  12480  bldisj  12609  blgt0  12610  bl2in  12611  blss2ps  12614  blss2  12615  xblm  12625  blssps  12635  blss  12636  xmetresbl  12648  bdbl  12711  bdmopn  12712  metcnp3  12719  metcnp  12720  metcnp2  12721  dvfvalap  12858  dvcnp2cntop  12871  dvcn  12872  logdivlti  13010