Theorem simpl2 1027

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

Assertion

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

Proof of Theorem simpl2

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

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

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 1006

This theorem is referenced by:  simpll2  1063  simprl2  1069  simp1l2  1117  simp2l2  1123  simp3l2  1129  3anandirs  1384  rspc3ev  2926  ifnetruedc  3650  tfisi  4687  brcogw  4901  oawordi  6642  nnmord  6690  nnmword  6691  1dom1el  6998  ac6sfi  7092  unsnfi  7116  unsnfidcel  7118  ordiso2  7239  prarloclemarch2  7644  enq0tr  7659  distrlem4prl  7809  distrlem4pru  7810  ltaprg  7844  aptiprlemu  7865  lelttr  8273  ltletr  8274  readdcan  8324  addcan  8364  addcan2  8365  ltadd2  8604  ltmul1a  8776  ltmul1  8777  divmulassap  8880  divmulasscomap  8881  lemul1a  9043  xrlelttr  10046  xrltletr  10047  xaddass  10109  xleadd1a  10113  xltadd1  10116  xlesubadd  10123  ixxdisj  10143  icoshftf1o  10231  icodisj  10232  lincmb01cmp  10243  iccf1o  10244  fztri3or  10279  ioom  10526  modqmuladdim  10635  modqmuladdnn0  10636  q2submod  10653  modqaddmulmod  10659  seqp1g  10734  exp3val  10809  ltexp2a  10859  exple1  10863  expnbnd  10931  expnlbnd2  10933  nn0ltexp2  10977  nn0leexp2  10978  mulsubdivbinom2ap  10979  expcan  10984  fiprsshashgt1  11087  hashtpgim  11115  hashtpg  11117  fun2dmnop0  11120  ccatass  11194  fzowrddc  11237  swrdclg  11240  ccatopth  11306  pfxccatin12lem2a  11317  maxleastb  11797  maxltsup  11801  xrltmaxsup  11840  xrmaxltsup  11841  xrmaxaddlem  11843  xrmaxadd  11844  addcn2  11893  mulcn2  11895  geoisum1c  12104  dvdsval2  12374  dvdsmodexp  12379  dvdsadd2b  12424  dvdsaddre2b  12425  dvdsmod  12446  oexpneg  12461  divalglemex  12506  divalg  12508  gcdass  12609  rplpwr  12621  rppwr  12622  nnminle  12629  lcmass  12680  coprmdvds2  12688  rpmulgcd2  12690  rpdvds  12694  cncongr2  12699  rpexp  12748  znege1  12773  prmdiveq  12831  hashgcdlem  12833  odzdvds  12841  coprimeprodsq2  12854  pythagtriplem3  12863  pythagtriplem4  12864  pcdvdsb  12916  pcbc  12947  ctinf  13074  nninfdc  13097  isnsgrp  13512  issubmnd  13548  nmzsubg  13820  ghmnsgima  13878  srg1zr  14024  ring1eq0  14085  mulgass2  14095  rhmdvdsr  14213  rmodislmod  14389  topssnei  14915  cnptopco  14975  cnconst2  14986  cnptoprest  14992  cnpdis  14995  upxp  15025  bldisj  15154  blgt0  15155  bl2in  15156  blss2ps  15159  blss2  15160  xblm  15170  blssps  15180  blss  15181  xmetresbl  15193  bdbl  15256  bdmopn  15257  metcnp3  15264  metcnp  15265  metcnp2  15266  dvfvalap  15434  dvcnp2cntop  15452  dvcn  15453  ply1term  15496  dvply1  15518  logdivlti  15634  ltexp2  15694  lgsfvalg  15763  lgsneg  15782  lgsdilem  15785  lgsdirprm  15792  lgsdir  15793  lgsdi  15795  lgsne0  15796  clwwlknonex2e  16320