Theorem simpl2 996

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

Assertion

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

Proof of Theorem simpl2

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

Syntax hints:   → wi 4   ∧ wa 103   ∧ w3a 973

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106

This theorem depends on definitions:  df-bi 116  df-3an 975

This theorem is referenced by:  simpll2  1032  simprl2  1038  simp1l2  1086  simp2l2  1092  simp3l2  1098  3anandirs  1343  rspc3ev  2851  tfisi  4569  brcogw  4778  oawordi  6446  nnmord  6494  nnmword  6495  ac6sfi  6874  unsnfi  6894  unsnfidcel  6896  ordiso2  7010  prarloclemarch2  7374  enq0tr  7389  distrlem4prl  7539  distrlem4pru  7540  ltaprg  7574  aptiprlemu  7595  lelttr  8001  ltletr  8002  readdcan  8052  addcan  8092  addcan2  8093  ltadd2  8331  ltmul1a  8503  ltmul1  8504  divmulassap  8605  divmulasscomap  8606  lemul1a  8767  xrlelttr  9756  xrltletr  9757  xaddass  9819  xleadd1a  9823  xltadd1  9826  xlesubadd  9833  ixxdisj  9853  icoshftf1o  9941  icodisj  9942  lincmb01cmp  9953  iccf1o  9954  fztri3or  9988  ioom  10210  modqmuladdim  10316  modqmuladdnn0  10317  q2submod  10334  modqaddmulmod  10340  exp3val  10471  ltexp2a  10521  exple1  10525  expnbnd  10592  expnlbnd2  10594  nn0ltexp2  10637  nn0leexp2  10638  expcan  10643  fiprsshashgt1  10745  maxleastb  11171  maxltsup  11175  xrltmaxsup  11213  xrmaxltsup  11214  xrmaxaddlem  11216  xrmaxadd  11217  addcn2  11266  mulcn2  11268  geoisum1c  11476  dvdsval2  11745  dvdsmodexp  11750  dvdsadd2b  11795  dvdsmod  11815  oexpneg  11829  divalglemex  11874  divalg  11876  gcdass  11963  rplpwr  11975  rppwr  11976  nnminle  11983  lcmass  12032  coprmdvds2  12040  rpmulgcd2  12042  rpdvds  12046  cncongr2  12051  rpexp  12100  znege1  12125  prmdiveq  12183  hashgcdlem  12185  odzdvds  12192  coprimeprodsq2  12205  pythagtriplem3  12214  pythagtriplem4  12215  pcdvdsb  12266  pcbc  12296  ctinf  12378  nninfdc  12401  isnsgrp  12640  topssnei  12921  cnptopco  12981  cnconst2  12992  cnptoprest  12998  cnpdis  13001  upxp  13031  bldisj  13160  blgt0  13161  bl2in  13162  blss2ps  13165  blss2  13166  xblm  13176  blssps  13186  blss  13187  xmetresbl  13199  bdbl  13262  bdmopn  13263  metcnp3  13270  metcnp  13271  metcnp2  13272  dvfvalap  13409  dvcnp2cntop  13422  dvcn  13423  logdivlti  13561  ltexp2  13619  lgsfvalg  13665  lgsneg  13684  lgsdilem  13687  lgsdirprm  13694  lgsdir  13695  lgsdi  13697  lgsne0  13698