Theorem simpl2 1027

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

Assertion

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

Proof of Theorem simpl2

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

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

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 1006

This theorem is referenced by:  simpll2  1063  simprl2  1069  simp1l2  1117  simp2l2  1123  simp3l2  1129  3anandirs  1384  rspc3ev  2927  ifnetruedc  3649  tfisi  4685  brcogw  4899  oawordi  6637  nnmord  6685  nnmword  6686  1dom1el  6993  ac6sfi  7087  unsnfi  7111  unsnfidcel  7113  ordiso2  7234  prarloclemarch2  7639  enq0tr  7654  distrlem4prl  7804  distrlem4pru  7805  ltaprg  7839  aptiprlemu  7860  lelttr  8268  ltletr  8269  readdcan  8319  addcan  8359  addcan2  8360  ltadd2  8599  ltmul1a  8771  ltmul1  8772  divmulassap  8875  divmulasscomap  8876  lemul1a  9038  xrlelttr  10041  xrltletr  10042  xaddass  10104  xleadd1a  10108  xltadd1  10111  xlesubadd  10118  ixxdisj  10138  icoshftf1o  10226  icodisj  10227  lincmb01cmp  10238  iccf1o  10239  fztri3or  10274  ioom  10521  modqmuladdim  10630  modqmuladdnn0  10631  q2submod  10648  modqaddmulmod  10654  seqp1g  10729  exp3val  10804  ltexp2a  10854  exple1  10858  expnbnd  10926  expnlbnd2  10928  nn0ltexp2  10972  nn0leexp2  10973  mulsubdivbinom2ap  10974  expcan  10979  fiprsshashgt1  11082  fun2dmnop0  11112  ccatass  11186  fzowrddc  11229  swrdclg  11232  ccatopth  11298  pfxccatin12lem2a  11309  maxleastb  11776  maxltsup  11780  xrltmaxsup  11819  xrmaxltsup  11820  xrmaxaddlem  11822  xrmaxadd  11823  addcn2  11872  mulcn2  11874  geoisum1c  12083  dvdsval2  12353  dvdsmodexp  12358  dvdsadd2b  12403  dvdsaddre2b  12404  dvdsmod  12425  oexpneg  12440  divalglemex  12485  divalg  12487  gcdass  12588  rplpwr  12600  rppwr  12601  nnminle  12608  lcmass  12659  coprmdvds2  12667  rpmulgcd2  12669  rpdvds  12673  cncongr2  12678  rpexp  12727  znege1  12752  prmdiveq  12810  hashgcdlem  12812  odzdvds  12820  coprimeprodsq2  12833  pythagtriplem3  12842  pythagtriplem4  12843  pcdvdsb  12895  pcbc  12926  ctinf  13053  nninfdc  13076  isnsgrp  13491  issubmnd  13527  nmzsubg  13799  ghmnsgima  13857  srg1zr  14003  ring1eq0  14064  mulgass2  14074  rhmdvdsr  14192  rmodislmod  14368  topssnei  14889  cnptopco  14949  cnconst2  14960  cnptoprest  14966  cnpdis  14969  upxp  14999  bldisj  15128  blgt0  15129  bl2in  15130  blss2ps  15133  blss2  15134  xblm  15144  blssps  15154  blss  15155  xmetresbl  15167  bdbl  15230  bdmopn  15231  metcnp3  15238  metcnp  15239  metcnp2  15240  dvfvalap  15408  dvcnp2cntop  15426  dvcn  15427  ply1term  15470  dvply1  15492  logdivlti  15608  ltexp2  15668  lgsfvalg  15737  lgsneg  15756  lgsdilem  15759  lgsdirprm  15766  lgsdir  15767  lgsdi  15769  lgsne0  15770  clwwlknonex2e  16294