Theorem simpl2 1032

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

Assertion

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

Proof of Theorem simpl2

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 104   ∧ w3a 1009

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107

This proof depends on definitions:  df-bi 117  df-3an 1011

This theorem is used by:  simpll2  1068  simprl2  1074  simp1l2  1122  simp2l2  1128  simp3l2  1134  3anandirs  1389  rspc3ev  2947  ifnetruedc  3684  tfisi  4734  brcogw  4949  oawordi  6742  nnmord  6790  nnmword  6791  1dom1el  7107  mapunen  7151  ac6sfi  7202  unsnfi  7226  unsnfidcel  7228  ordiso2  7375  prarloclemarch2  7786  enq0tr  7801  distrlem4prl  7951  distrlem4pru  7952  ltaprg  7986  aptiprlemu  8007  lelttr  8414  ltletr  8415  readdcan  8466  addcan  8506  addcan2  8507  ltadd2  8747  ltmul1a  8920  ltmul1  8921  divmulassap  9026  divmulasscomap  9027  lemul1a  9189  xrlelttr  10210  xrltletr  10211  xaddass  10273  xleadd1a  10277  xltadd1  10280  xlesubadd  10287  ixxdisj  10307  icoshftf1o  10395  icodisj  10396  lincmb01cmp  10407  lincmble  10408  iccf1o  10409  fztri3or  10445  ioom  10697  modqmuladdim  10806  modqmuladdnn0  10807  q2submod  10824  modqaddmulmod  10830  seqp1g  10905  exp3val  10980  ltexp2a  11030  exple1  11034  expnbnd  11103  expnlbnd2  11105  nn0ltexp2  11149  nn0leexp2  11150  mulsubdivbinom2ap  11151  expcan  11156  fiprsshashgt1  11260  hashtpgim  11299  hashtpg  11301  fun2dmnop0  11304  ccatass  11378  fzowrddc  11421  swrdclg  11424  ccatopth  11490  pfxccatin12lem2a  11501  maxleastb  11982  maxltsup  11986  xrltmaxsup  12025  xrmaxltsup  12026  xrmaxaddlem  12028  xrmaxadd  12029  addcn2  12078  mulcn2  12080  geoisum1c  12289  dvdsval2  12559  dvdsmodexp  12564  dvdsadd2b  12609  dvdsaddre2b  12610  dvdsmod  12631  oexpneg  12646  divalglemex  12691  divalg  12693  gcdass  12794  rplpwr  12806  rppwr  12807  nnminle  12814  lcmass  12865  coprmdvds2  12873  rpmulgcd2  12875  rpdvds  12879  cncongr2  12884  rpexp  12933  znege1  12958  prmdiveq  13016  hashgcdlem  13018  odzdvds  13026  coprimeprodsq2  13039  pythagtriplem3  13048  pythagtriplem4  13049  pcdvdsb  13101  pcbc  13132  ctinf  13323  nninfdc  13346  isnsgrp  13723  issubmnd  13757  nmzsubg  14015  ghmnsgima  14073  ring1eq0  14355  mulgass2  14365  rhmdvdsr  14484  rmodislmod  14690  issubassa  15015  topssnei  15265  cnptopco  15325  cnconst2  15336  cnptoprest  15342  cnpdis  15345  upxp  15375  bldisj  15504  blgt0  15505  bl2in  15506  blss2ps  15509  blss2  15510  xblm  15520  blssps  15530  blss  15531  xmetresbl  15543  bdbl  15606  bdmopn  15607  metcnp3  15614  metcnp  15615  metcnp2  15616  dvfvalap  15784  dvcnp2cntop  15802  dvcn  15803  ply1term  15846  dvply1  15868  logdivlti  15986  ltexp2  16049  pellexlem2  16098  bcmono  16124  lgsfvalg  16136  lgsneg  16155  lgsdilem  16158  lgsdirprm  16165  lgsdir  16166  lgsdi  16168  lgsne0  16169  clwwlknonex2e  16693