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  4736  brcogw  4951  oawordi  6746  nnmord  6794  nnmword  6795  1dom1el  7112  mapunen  7156  ac6sfi  7207  unsnfi  7231  unsnfidcel  7233  ordiso2  7382  prarloclemarch2  7793  enq0tr  7808  distrlem4prl  7958  distrlem4pru  7959  ltaprg  7993  aptiprlemu  8014  lelttr  8421  ltletr  8422  readdcan  8474  addcan  8514  addcan2  8515  ltadd2  8755  ltmul1a  8928  ltmul1  8929  divmulassap  9034  divmulasscomap  9035  lemul1a  9197  xrlelttr  10226  xrltletr  10227  xaddass  10289  xleadd1a  10293  xltadd1  10296  xlesubadd  10303  ixxdisj  10323  icoshftf1o  10411  icodisj  10412  lincmb01cmp  10423  lincmble  10424  iccf1o  10425  fztri3or  10461  ioom  10713  modqmuladdim  10826  modqmuladdnn0  10827  q2submod  10844  modqaddmulmod  10850  seqp1g  10925  exp3val  11000  ltexp2a  11050  exple1  11054  expnbnd  11123  expnlbnd2  11125  nn0ltexp2  11170  nn0leexp2  11171  mulsubdivbinom2ap  11172  expcan  11177  fiprsshashgt1  11281  hashtpgim  11320  hashtpg  11322  fun2dmnop0  11325  ccatass  11399  fzowrddc  11442  swrdclg  11445  ccatopth  11511  pfxccatin12lem2a  11522  maxleastb  12004  maxltsup  12008  xrltmaxsup  12049  xrmaxltsup  12050  xrmaxaddlem  12052  xrmaxadd  12053  addcn2  12102  mulcn2  12104  geoisum1c  12313  dvdsval2  12583  dvdsmodexp  12588  dvdsadd2b  12633  dvdsaddre2b  12634  dvdsmod  12655  oexpneg  12670  divalglemex  12715  divalg  12717  gcdass  12818  rplpwr  12830  rppwr  12831  nnminle  12838  lcmass  12889  coprmdvds2  12897  rpmulgcd2  12899  rpdvds  12903  cncongr2  12908  rpexp  12958  znege1  12984  prmdiveq  13044  hashgcdlem  13046  odzdvds  13054  coprimeprodsq2  13067  pythagtriplem3  13076  pythagtriplem4  13077  pcdvdsb  13129  pcbc  13160  ctinf  13380  nninfdc  13403  isnsgrp  13781  issubmnd  13815  nmzsubg  14073  ghmnsgima  14131  ring1eq0  14461  mulgass2  14471  rhmdvdsr  14592  rmodislmod  14798  issubassa  15123  snifpsrbagfi  15170  topssnei  15400  cnptopco  15460  cnconst2  15471  cnptoprest  15477  cnpdis  15480  upxp  15510  bldisj  15639  blgt0  15640  bl2in  15641  blss2ps  15644  blss2  15645  xblm  15655  blssps  15665  blss  15666  xmetresbl  15678  bdbl  15741  bdmopn  15742  metcnp3  15749  metcnp  15750  metcnp2  15751  dvfvalap  15919  dvcnp2cntop  15937  dvcn  15938  ply1term  15981  dvply1  16003  logdivlti  16123  efnthr  16188  ltexp2  16189  pellexlem2  16242  bcmono  16316  lgsfvalg  16341  lgsneg  16360  lgsdilem  16363  lgsdirprm  16370  lgsdir  16371  lgsdi  16373  lgsne0  16374  clwwlknonex2e  16898