Theorem simpl2 1003

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

Assertion

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

Proof of Theorem simpl2

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

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

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 982

This theorem is referenced by:  simpll2  1039  simprl2  1045  simp1l2  1093  simp2l2  1099  simp3l2  1105  3anandirs  1359  rspc3ev  2885  ifnetruedc  3603  tfisi  4624  brcogw  4836  oawordi  6536  nnmord  6584  nnmword  6585  ac6sfi  6968  unsnfi  6989  unsnfidcel  6991  ordiso2  7110  prarloclemarch2  7505  enq0tr  7520  distrlem4prl  7670  distrlem4pru  7671  ltaprg  7705  aptiprlemu  7726  lelttr  8134  ltletr  8135  readdcan  8185  addcan  8225  addcan2  8226  ltadd2  8465  ltmul1a  8637  ltmul1  8638  divmulassap  8741  divmulasscomap  8742  lemul1a  8904  xrlelttr  9900  xrltletr  9901  xaddass  9963  xleadd1a  9967  xltadd1  9970  xlesubadd  9977  ixxdisj  9997  icoshftf1o  10085  icodisj  10086  lincmb01cmp  10097  iccf1o  10098  fztri3or  10133  ioom  10369  modqmuladdim  10478  modqmuladdnn0  10479  q2submod  10496  modqaddmulmod  10502  seqp1g  10577  exp3val  10652  ltexp2a  10702  exple1  10706  expnbnd  10774  expnlbnd2  10776  nn0ltexp2  10820  nn0leexp2  10821  mulsubdivbinom2ap  10822  expcan  10827  fiprsshashgt1  10928  maxleastb  11398  maxltsup  11402  xrltmaxsup  11441  xrmaxltsup  11442  xrmaxaddlem  11444  xrmaxadd  11445  addcn2  11494  mulcn2  11496  geoisum1c  11704  dvdsval2  11974  dvdsmodexp  11979  dvdsadd2b  12024  dvdsaddre2b  12025  dvdsmod  12046  oexpneg  12061  divalglemex  12106  divalg  12108  gcdass  12209  rplpwr  12221  rppwr  12222  nnminle  12229  lcmass  12280  coprmdvds2  12288  rpmulgcd2  12290  rpdvds  12294  cncongr2  12299  rpexp  12348  znege1  12373  prmdiveq  12431  hashgcdlem  12433  odzdvds  12441  coprimeprodsq2  12454  pythagtriplem3  12463  pythagtriplem4  12464  pcdvdsb  12516  pcbc  12547  ctinf  12674  nninfdc  12697  isnsgrp  13110  issubmnd  13146  nmzsubg  13418  ghmnsgima  13476  srg1zr  13621  ring1eq0  13682  mulgass2  13692  rhmdvdsr  13809  rmodislmod  13985  topssnei  14484  cnptopco  14544  cnconst2  14555  cnptoprest  14561  cnpdis  14564  upxp  14594  bldisj  14723  blgt0  14724  bl2in  14725  blss2ps  14728  blss2  14729  xblm  14739  blssps  14749  blss  14750  xmetresbl  14762  bdbl  14825  bdmopn  14826  metcnp3  14833  metcnp  14834  metcnp2  14835  dvfvalap  15003  dvcnp2cntop  15021  dvcn  15022  ply1term  15065  dvply1  15087  logdivlti  15203  ltexp2  15263  lgsfvalg  15332  lgsneg  15351  lgsdilem  15354  lgsdirprm  15361  lgsdir  15362  lgsdi  15364  lgsne0  15365  1dom1el  15723