Theorem simpl2 1028

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

Assertion

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

Proof of Theorem simpl2

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

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

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 1007

This theorem is referenced by:  simpll2  1064  simprl2  1070  simp1l2  1118  simp2l2  1124  simp3l2  1130  3anandirs  1385  rspc3ev  2937  ifnetruedc  3665  tfisi  4708  brcogw  4923  oawordi  6701  nnmord  6749  nnmword  6750  1dom1el  7059  mapunen  7103  ac6sfi  7154  unsnfi  7178  unsnfidcel  7180  ordiso2  7325  prarloclemarch2  7730  enq0tr  7745  distrlem4prl  7895  distrlem4pru  7896  ltaprg  7930  aptiprlemu  7951  lelttr  8358  ltletr  8359  readdcan  8409  addcan  8449  addcan2  8450  ltadd2  8689  ltmul1a  8861  ltmul1  8862  divmulassap  8965  divmulasscomap  8966  lemul1a  9128  xrlelttr  10135  xrltletr  10136  xaddass  10198  xleadd1a  10202  xltadd1  10205  xlesubadd  10212  ixxdisj  10232  icoshftf1o  10320  icodisj  10321  lincmb01cmp  10332  lincmble  10333  iccf1o  10334  fztri3or  10369  ioom  10616  modqmuladdim  10725  modqmuladdnn0  10726  q2submod  10743  modqaddmulmod  10749  seqp1g  10824  exp3val  10899  ltexp2a  10949  exple1  10953  expnbnd  11021  expnlbnd2  11023  nn0ltexp2  11067  nn0leexp2  11068  mulsubdivbinom2ap  11069  expcan  11074  fiprsshashgt1  11177  hashtpgim  11210  hashtpg  11212  fun2dmnop0  11215  ccatass  11289  fzowrddc  11332  swrdclg  11335  ccatopth  11401  pfxccatin12lem2a  11412  maxleastb  11892  maxltsup  11896  xrltmaxsup  11935  xrmaxltsup  11936  xrmaxaddlem  11938  xrmaxadd  11939  addcn2  11988  mulcn2  11990  geoisum1c  12199  dvdsval2  12469  dvdsmodexp  12474  dvdsadd2b  12519  dvdsaddre2b  12520  dvdsmod  12541  oexpneg  12556  divalglemex  12601  divalg  12603  gcdass  12704  rplpwr  12716  rppwr  12717  nnminle  12724  lcmass  12775  coprmdvds2  12783  rpmulgcd2  12785  rpdvds  12789  cncongr2  12794  rpexp  12843  znege1  12868  prmdiveq  12926  hashgcdlem  12928  odzdvds  12936  coprimeprodsq2  12949  pythagtriplem3  12958  pythagtriplem4  12959  pcdvdsb  13011  pcbc  13042  ctinf  13170  nninfdc  13193  isnsgrp  13608  issubmnd  13644  nmzsubg  13916  ghmnsgima  13974  srg1zr  14120  ring1eq0  14181  mulgass2  14191  rhmdvdsr  14309  rmodislmod  14486  topssnei  15014  cnptopco  15074  cnconst2  15085  cnptoprest  15091  cnpdis  15094  upxp  15124  bldisj  15253  blgt0  15254  bl2in  15255  blss2ps  15258  blss2  15259  xblm  15269  blssps  15279  blss  15280  xmetresbl  15292  bdbl  15355  bdmopn  15356  metcnp3  15363  metcnp  15364  metcnp2  15365  dvfvalap  15533  dvcnp2cntop  15551  dvcn  15552  ply1term  15595  dvply1  15617  logdivlti  15733  ltexp2  15793  pellexlem2  15833  lgsfvalg  15865  lgsneg  15884  lgsdilem  15887  lgsdirprm  15894  lgsdir  15895  lgsdi  15897  lgsne0  15898  clwwlknonex2e  16422