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  2941  ifnetruedc  3670  tfisi  4714  brcogw  4929  oawordi  6715  nnmord  6763  nnmword  6764  1dom1el  7073  mapunen  7117  ac6sfi  7168  unsnfi  7192  unsnfidcel  7194  ordiso2  7339  prarloclemarch2  7750  enq0tr  7765  distrlem4prl  7915  distrlem4pru  7916  ltaprg  7950  aptiprlemu  7971  lelttr  8378  ltletr  8379  readdcan  8430  addcan  8470  addcan2  8471  ltadd2  8711  ltmul1a  8883  ltmul1  8884  divmulassap  8989  divmulasscomap  8990  lemul1a  9152  xrlelttr  10161  xrltletr  10162  xaddass  10224  xleadd1a  10228  xltadd1  10231  xlesubadd  10238  ixxdisj  10258  icoshftf1o  10346  icodisj  10347  lincmb01cmp  10358  lincmble  10359  iccf1o  10360  fztri3or  10396  ioom  10647  modqmuladdim  10756  modqmuladdnn0  10757  q2submod  10774  modqaddmulmod  10780  seqp1g  10855  exp3val  10930  ltexp2a  10980  exple1  10984  expnbnd  11053  expnlbnd2  11055  nn0ltexp2  11099  nn0leexp2  11100  mulsubdivbinom2ap  11101  expcan  11106  fiprsshashgt1  11210  hashtpgim  11245  hashtpg  11247  fun2dmnop0  11250  ccatass  11324  fzowrddc  11367  swrdclg  11370  ccatopth  11436  pfxccatin12lem2a  11447  maxleastb  11927  maxltsup  11931  xrltmaxsup  11970  xrmaxltsup  11971  xrmaxaddlem  11973  xrmaxadd  11974  addcn2  12023  mulcn2  12025  geoisum1c  12234  dvdsval2  12504  dvdsmodexp  12509  dvdsadd2b  12554  dvdsaddre2b  12555  dvdsmod  12576  oexpneg  12591  divalglemex  12636  divalg  12638  gcdass  12739  rplpwr  12751  rppwr  12752  nnminle  12759  lcmass  12810  coprmdvds2  12818  rpmulgcd2  12820  rpdvds  12824  cncongr2  12829  rpexp  12878  znege1  12903  prmdiveq  12961  hashgcdlem  12963  odzdvds  12971  coprimeprodsq2  12984  pythagtriplem3  12993  pythagtriplem4  12994  pcdvdsb  13046  pcbc  13077  ctinf  13268  nninfdc  13291  isnsgrp  13672  issubmnd  13706  nmzsubg  13966  ghmnsgima  14024  ring1eq0  14294  mulgass2  14304  rhmdvdsr  14423  rmodislmod  14628  topssnei  15156  cnptopco  15216  cnconst2  15227  cnptoprest  15233  cnpdis  15236  upxp  15266  bldisj  15395  blgt0  15396  bl2in  15397  blss2ps  15400  blss2  15401  xblm  15411  blssps  15421  blss  15422  xmetresbl  15434  bdbl  15497  bdmopn  15498  metcnp3  15505  metcnp  15506  metcnp2  15507  dvfvalap  15675  dvcnp2cntop  15693  dvcn  15694  ply1term  15737  dvply1  15759  logdivlti  15875  ltexp2  15935  pellexlem2  15975  lgsfvalg  16007  lgsneg  16026  lgsdilem  16029  lgsdirprm  16036  lgsdir  16037  lgsdi  16039  lgsne0  16040  clwwlknonex2e  16564