Theorem simpl2 1004

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

Assertion

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

Proof of Theorem simpl2

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

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

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 983

This theorem is referenced by:  simpll2  1040  simprl2  1046  simp1l2  1094  simp2l2  1100  simp3l2  1106  3anandirs  1361  rspc3ev  2895  ifnetruedc  3614  tfisi  4639  brcogw  4851  oawordi  6562  nnmord  6610  nnmword  6611  ac6sfi  7002  unsnfi  7023  unsnfidcel  7025  ordiso2  7144  prarloclemarch2  7539  enq0tr  7554  distrlem4prl  7704  distrlem4pru  7705  ltaprg  7739  aptiprlemu  7760  lelttr  8168  ltletr  8169  readdcan  8219  addcan  8259  addcan2  8260  ltadd2  8499  ltmul1a  8671  ltmul1  8672  divmulassap  8775  divmulasscomap  8776  lemul1a  8938  xrlelttr  9935  xrltletr  9936  xaddass  9998  xleadd1a  10002  xltadd1  10005  xlesubadd  10012  ixxdisj  10032  icoshftf1o  10120  icodisj  10121  lincmb01cmp  10132  iccf1o  10133  fztri3or  10168  ioom  10410  modqmuladdim  10519  modqmuladdnn0  10520  q2submod  10537  modqaddmulmod  10543  seqp1g  10618  exp3val  10693  ltexp2a  10743  exple1  10747  expnbnd  10815  expnlbnd2  10817  nn0ltexp2  10861  nn0leexp2  10862  mulsubdivbinom2ap  10863  expcan  10868  fiprsshashgt1  10969  fun2dmnop0  10999  ccatass  11072  fzowrddc  11108  swrdclg  11111  maxleastb  11569  maxltsup  11573  xrltmaxsup  11612  xrmaxltsup  11613  xrmaxaddlem  11615  xrmaxadd  11616  addcn2  11665  mulcn2  11667  geoisum1c  11875  dvdsval2  12145  dvdsmodexp  12150  dvdsadd2b  12195  dvdsaddre2b  12196  dvdsmod  12217  oexpneg  12232  divalglemex  12277  divalg  12279  gcdass  12380  rplpwr  12392  rppwr  12393  nnminle  12400  lcmass  12451  coprmdvds2  12459  rpmulgcd2  12461  rpdvds  12465  cncongr2  12470  rpexp  12519  znege1  12544  prmdiveq  12602  hashgcdlem  12604  odzdvds  12612  coprimeprodsq2  12625  pythagtriplem3  12634  pythagtriplem4  12635  pcdvdsb  12687  pcbc  12718  ctinf  12845  nninfdc  12868  isnsgrp  13282  issubmnd  13318  nmzsubg  13590  ghmnsgima  13648  srg1zr  13793  ring1eq0  13854  mulgass2  13864  rhmdvdsr  13981  rmodislmod  14157  topssnei  14678  cnptopco  14738  cnconst2  14749  cnptoprest  14755  cnpdis  14758  upxp  14788  bldisj  14917  blgt0  14918  bl2in  14919  blss2ps  14922  blss2  14923  xblm  14933  blssps  14943  blss  14944  xmetresbl  14956  bdbl  15019  bdmopn  15020  metcnp3  15027  metcnp  15028  metcnp2  15029  dvfvalap  15197  dvcnp2cntop  15215  dvcn  15216  ply1term  15259  dvply1  15281  logdivlti  15397  ltexp2  15457  lgsfvalg  15526  lgsneg  15545  lgsdilem  15548  lgsdirprm  15555  lgsdir  15556  lgsdi  15558  lgsne0  15559  1dom1el  16001