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  2940  ifnetruedc  3668  tfisi  4711  brcogw  4926  oawordi  6704  nnmord  6752  nnmword  6753  1dom1el  7062  mapunen  7106  ac6sfi  7157  unsnfi  7181  unsnfidcel  7183  ordiso2  7328  prarloclemarch2  7739  enq0tr  7754  distrlem4prl  7904  distrlem4pru  7905  ltaprg  7939  aptiprlemu  7960  lelttr  8367  ltletr  8368  readdcan  8418  addcan  8458  addcan2  8459  ltadd2  8698  ltmul1a  8870  ltmul1  8871  divmulassap  8974  divmulasscomap  8975  lemul1a  9137  xrlelttr  10145  xrltletr  10146  xaddass  10208  xleadd1a  10212  xltadd1  10215  xlesubadd  10222  ixxdisj  10242  icoshftf1o  10330  icodisj  10331  lincmb01cmp  10342  lincmble  10343  iccf1o  10344  fztri3or  10379  ioom  10627  modqmuladdim  10736  modqmuladdnn0  10737  q2submod  10754  modqaddmulmod  10760  seqp1g  10835  exp3val  10910  ltexp2a  10960  exple1  10964  expnbnd  11033  expnlbnd2  11035  nn0ltexp2  11079  nn0leexp2  11080  mulsubdivbinom2ap  11081  expcan  11086  fiprsshashgt1  11190  hashtpgim  11225  hashtpg  11227  fun2dmnop0  11230  ccatass  11304  fzowrddc  11347  swrdclg  11350  ccatopth  11416  pfxccatin12lem2a  11427  maxleastb  11907  maxltsup  11911  xrltmaxsup  11950  xrmaxltsup  11951  xrmaxaddlem  11953  xrmaxadd  11954  addcn2  12003  mulcn2  12005  geoisum1c  12214  dvdsval2  12484  dvdsmodexp  12489  dvdsadd2b  12534  dvdsaddre2b  12535  dvdsmod  12556  oexpneg  12571  divalglemex  12616  divalg  12618  gcdass  12719  rplpwr  12731  rppwr  12732  nnminle  12739  lcmass  12790  coprmdvds2  12798  rpmulgcd2  12800  rpdvds  12804  cncongr2  12809  rpexp  12858  znege1  12883  prmdiveq  12941  hashgcdlem  12943  odzdvds  12951  coprimeprodsq2  12964  pythagtriplem3  12973  pythagtriplem4  12974  pcdvdsb  13026  pcbc  13057  ctinf  13202  nninfdc  13225  isnsgrp  13640  issubmnd  13676  nmzsubg  13948  ghmnsgima  14006  srg1zr  14152  ring1eq0  14213  mulgass2  14223  rhmdvdsr  14342  rmodislmod  14548  topssnei  15076  cnptopco  15136  cnconst2  15147  cnptoprest  15153  cnpdis  15156  upxp  15186  bldisj  15315  blgt0  15316  bl2in  15317  blss2ps  15320  blss2  15321  xblm  15331  blssps  15341  blss  15342  xmetresbl  15354  bdbl  15417  bdmopn  15418  metcnp3  15425  metcnp  15426  metcnp2  15427  dvfvalap  15595  dvcnp2cntop  15613  dvcn  15614  ply1term  15657  dvply1  15679  logdivlti  15795  ltexp2  15855  pellexlem2  15895  lgsfvalg  15927  lgsneg  15946  lgsdilem  15949  lgsdirprm  15956  lgsdir  15957  lgsdi  15959  lgsne0  15960  clwwlknonex2e  16484