Theorem simpl2 1025

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

Assertion

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

Proof of Theorem simpl2

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

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

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 1004

This theorem is referenced by:  simpll2  1061  simprl2  1067  simp1l2  1115  simp2l2  1121  simp3l2  1127  3anandirs  1382  rspc3ev  2925  ifnetruedc  3647  tfisi  4683  brcogw  4897  oawordi  6632  nnmord  6680  nnmword  6681  1dom1el  6988  ac6sfi  7082  unsnfi  7106  unsnfidcel  7108  ordiso2  7228  prarloclemarch2  7632  enq0tr  7647  distrlem4prl  7797  distrlem4pru  7798  ltaprg  7832  aptiprlemu  7853  lelttr  8261  ltletr  8262  readdcan  8312  addcan  8352  addcan2  8353  ltadd2  8592  ltmul1a  8764  ltmul1  8765  divmulassap  8868  divmulasscomap  8869  lemul1a  9031  xrlelttr  10034  xrltletr  10035  xaddass  10097  xleadd1a  10101  xltadd1  10104  xlesubadd  10111  ixxdisj  10131  icoshftf1o  10219  icodisj  10220  lincmb01cmp  10231  iccf1o  10232  fztri3or  10267  ioom  10513  modqmuladdim  10622  modqmuladdnn0  10623  q2submod  10640  modqaddmulmod  10646  seqp1g  10721  exp3val  10796  ltexp2a  10846  exple1  10850  expnbnd  10918  expnlbnd2  10920  nn0ltexp2  10964  nn0leexp2  10965  mulsubdivbinom2ap  10966  expcan  10971  fiprsshashgt1  11074  fun2dmnop0  11104  ccatass  11178  fzowrddc  11221  swrdclg  11224  ccatopth  11290  pfxccatin12lem2a  11301  maxleastb  11768  maxltsup  11772  xrltmaxsup  11811  xrmaxltsup  11812  xrmaxaddlem  11814  xrmaxadd  11815  addcn2  11864  mulcn2  11866  geoisum1c  12074  dvdsval2  12344  dvdsmodexp  12349  dvdsadd2b  12394  dvdsaddre2b  12395  dvdsmod  12416  oexpneg  12431  divalglemex  12476  divalg  12478  gcdass  12579  rplpwr  12591  rppwr  12592  nnminle  12599  lcmass  12650  coprmdvds2  12658  rpmulgcd2  12660  rpdvds  12664  cncongr2  12669  rpexp  12718  znege1  12743  prmdiveq  12801  hashgcdlem  12803  odzdvds  12811  coprimeprodsq2  12824  pythagtriplem3  12833  pythagtriplem4  12834  pcdvdsb  12886  pcbc  12917  ctinf  13044  nninfdc  13067  isnsgrp  13482  issubmnd  13518  nmzsubg  13790  ghmnsgima  13848  srg1zr  13993  ring1eq0  14054  mulgass2  14064  rhmdvdsr  14182  rmodislmod  14358  topssnei  14879  cnptopco  14939  cnconst2  14950  cnptoprest  14956  cnpdis  14959  upxp  14989  bldisj  15118  blgt0  15119  bl2in  15120  blss2ps  15123  blss2  15124  xblm  15134  blssps  15144  blss  15145  xmetresbl  15157  bdbl  15220  bdmopn  15221  metcnp3  15228  metcnp  15229  metcnp2  15230  dvfvalap  15398  dvcnp2cntop  15416  dvcn  15417  ply1term  15460  dvply1  15482  logdivlti  15598  ltexp2  15658  lgsfvalg  15727  lgsneg  15746  lgsdilem  15749  lgsdirprm  15756  lgsdir  15757  lgsdi  15759  lgsne0  15760  clwwlknonex2e  16249