Theorem simpl2 1001

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

Assertion

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

Proof of Theorem simpl2

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

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

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 980

This theorem is referenced by:  simpll2  1037  simprl2  1043  simp1l2  1091  simp2l2  1097  simp3l2  1103  3anandirs  1348  rspc3ev  2858  tfisi  4586  brcogw  4796  oawordi  6469  nnmord  6517  nnmword  6518  ac6sfi  6897  unsnfi  6917  unsnfidcel  6919  ordiso2  7033  prarloclemarch2  7417  enq0tr  7432  distrlem4prl  7582  distrlem4pru  7583  ltaprg  7617  aptiprlemu  7638  lelttr  8045  ltletr  8046  readdcan  8096  addcan  8136  addcan2  8137  ltadd2  8375  ltmul1a  8547  ltmul1  8548  divmulassap  8651  divmulasscomap  8652  lemul1a  8814  xrlelttr  9805  xrltletr  9806  xaddass  9868  xleadd1a  9872  xltadd1  9875  xlesubadd  9882  ixxdisj  9902  icoshftf1o  9990  icodisj  9991  lincmb01cmp  10002  iccf1o  10003  fztri3or  10038  ioom  10260  modqmuladdim  10366  modqmuladdnn0  10367  q2submod  10384  modqaddmulmod  10390  exp3val  10521  ltexp2a  10571  exple1  10575  expnbnd  10643  expnlbnd2  10645  nn0ltexp2  10688  nn0leexp2  10689  mulsubdivbinom2ap  10690  expcan  10695  fiprsshashgt1  10796  maxleastb  11222  maxltsup  11226  xrltmaxsup  11264  xrmaxltsup  11265  xrmaxaddlem  11267  xrmaxadd  11268  addcn2  11317  mulcn2  11319  geoisum1c  11527  dvdsval2  11796  dvdsmodexp  11801  dvdsadd2b  11846  dvdsaddre2b  11847  dvdsmod  11867  oexpneg  11881  divalglemex  11926  divalg  11928  gcdass  12015  rplpwr  12027  rppwr  12028  nnminle  12035  lcmass  12084  coprmdvds2  12092  rpmulgcd2  12094  rpdvds  12098  cncongr2  12103  rpexp  12152  znege1  12177  prmdiveq  12235  hashgcdlem  12237  odzdvds  12244  coprimeprodsq2  12257  pythagtriplem3  12266  pythagtriplem4  12267  pcdvdsb  12318  pcbc  12348  ctinf  12430  nninfdc  12453  isnsgrp  12811  issubmnd  12842  nmzsubg  13068  srg1zr  13168  ring1eq0  13223  mulgass2  13233  topssnei  13632  cnptopco  13692  cnconst2  13703  cnptoprest  13709  cnpdis  13712  upxp  13742  bldisj  13871  blgt0  13872  bl2in  13873  blss2ps  13876  blss2  13877  xblm  13887  blssps  13897  blss  13898  xmetresbl  13910  bdbl  13973  bdmopn  13974  metcnp3  13981  metcnp  13982  metcnp2  13983  dvfvalap  14120  dvcnp2cntop  14133  dvcn  14134  logdivlti  14272  ltexp2  14330  lgsfvalg  14376  lgsneg  14395  lgsdilem  14398  lgsdirprm  14405  lgsdir  14406  lgsdi  14408  lgsne0  14409