Theorem simpl2 1006

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

Assertion

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

Proof of Theorem simpl2

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

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

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 985

This theorem is referenced by:  simpll2  1042  simprl2  1048  simp1l2  1096  simp2l2  1102  simp3l2  1108  3anandirs  1363  rspc3ev  2904  ifnetruedc  3626  tfisi  4656  brcogw  4868  oawordi  6585  nnmord  6633  nnmword  6634  ac6sfi  7028  unsnfi  7049  unsnfidcel  7051  ordiso2  7170  prarloclemarch2  7574  enq0tr  7589  distrlem4prl  7739  distrlem4pru  7740  ltaprg  7774  aptiprlemu  7795  lelttr  8203  ltletr  8204  readdcan  8254  addcan  8294  addcan2  8295  ltadd2  8534  ltmul1a  8706  ltmul1  8707  divmulassap  8810  divmulasscomap  8811  lemul1a  8973  xrlelttr  9970  xrltletr  9971  xaddass  10033  xleadd1a  10037  xltadd1  10040  xlesubadd  10047  ixxdisj  10067  icoshftf1o  10155  icodisj  10156  lincmb01cmp  10167  iccf1o  10168  fztri3or  10203  ioom  10447  modqmuladdim  10556  modqmuladdnn0  10557  q2submod  10574  modqaddmulmod  10580  seqp1g  10655  exp3val  10730  ltexp2a  10780  exple1  10784  expnbnd  10852  expnlbnd2  10854  nn0ltexp2  10898  nn0leexp2  10899  mulsubdivbinom2ap  10900  expcan  10905  fiprsshashgt1  11006  fun2dmnop0  11036  ccatass  11109  fzowrddc  11145  swrdclg  11148  ccatopth  11214  pfxccatin12lem2a  11225  maxleastb  11691  maxltsup  11695  xrltmaxsup  11734  xrmaxltsup  11735  xrmaxaddlem  11737  xrmaxadd  11738  addcn2  11787  mulcn2  11789  geoisum1c  11997  dvdsval2  12267  dvdsmodexp  12272  dvdsadd2b  12317  dvdsaddre2b  12318  dvdsmod  12339  oexpneg  12354  divalglemex  12399  divalg  12401  gcdass  12502  rplpwr  12514  rppwr  12515  nnminle  12522  lcmass  12573  coprmdvds2  12581  rpmulgcd2  12583  rpdvds  12587  cncongr2  12592  rpexp  12641  znege1  12666  prmdiveq  12724  hashgcdlem  12726  odzdvds  12734  coprimeprodsq2  12747  pythagtriplem3  12756  pythagtriplem4  12757  pcdvdsb  12809  pcbc  12840  ctinf  12967  nninfdc  12990  isnsgrp  13405  issubmnd  13441  nmzsubg  13713  ghmnsgima  13771  srg1zr  13916  ring1eq0  13977  mulgass2  13987  rhmdvdsr  14104  rmodislmod  14280  topssnei  14801  cnptopco  14861  cnconst2  14872  cnptoprest  14878  cnpdis  14881  upxp  14911  bldisj  15040  blgt0  15041  bl2in  15042  blss2ps  15045  blss2  15046  xblm  15056  blssps  15066  blss  15067  xmetresbl  15079  bdbl  15142  bdmopn  15143  metcnp3  15150  metcnp  15151  metcnp2  15152  dvfvalap  15320  dvcnp2cntop  15338  dvcn  15339  ply1term  15382  dvply1  15404  logdivlti  15520  ltexp2  15580  lgsfvalg  15649  lgsneg  15668  lgsdilem  15671  lgsdirprm  15678  lgsdir  15679  lgsdi  15681  lgsne0  15682  1dom1el  16264