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  2882  ifnetruedc  3599  tfisi  4620  brcogw  4832  oawordi  6524  nnmord  6572  nnmword  6573  ac6sfi  6956  unsnfi  6977  unsnfidcel  6979  ordiso2  7096  prarloclemarch2  7481  enq0tr  7496  distrlem4prl  7646  distrlem4pru  7647  ltaprg  7681  aptiprlemu  7702  lelttr  8110  ltletr  8111  readdcan  8161  addcan  8201  addcan2  8202  ltadd2  8440  ltmul1a  8612  ltmul1  8613  divmulassap  8716  divmulasscomap  8717  lemul1a  8879  xrlelttr  9875  xrltletr  9876  xaddass  9938  xleadd1a  9942  xltadd1  9945  xlesubadd  9952  ixxdisj  9972  icoshftf1o  10060  icodisj  10061  lincmb01cmp  10072  iccf1o  10073  fztri3or  10108  ioom  10332  modqmuladdim  10441  modqmuladdnn0  10442  q2submod  10459  modqaddmulmod  10465  seqp1g  10540  exp3val  10615  ltexp2a  10665  exple1  10669  expnbnd  10737  expnlbnd2  10739  nn0ltexp2  10783  nn0leexp2  10784  mulsubdivbinom2ap  10785  expcan  10790  fiprsshashgt1  10891  maxleastb  11361  maxltsup  11365  xrltmaxsup  11403  xrmaxltsup  11404  xrmaxaddlem  11406  xrmaxadd  11407  addcn2  11456  mulcn2  11458  geoisum1c  11666  dvdsval2  11936  dvdsmodexp  11941  dvdsadd2b  11986  dvdsaddre2b  11987  dvdsmod  12007  oexpneg  12021  divalglemex  12066  divalg  12068  gcdass  12155  rplpwr  12167  rppwr  12168  nnminle  12175  lcmass  12226  coprmdvds2  12234  rpmulgcd2  12236  rpdvds  12240  cncongr2  12245  rpexp  12294  znege1  12319  prmdiveq  12377  hashgcdlem  12379  odzdvds  12386  coprimeprodsq2  12399  pythagtriplem3  12408  pythagtriplem4  12409  pcdvdsb  12461  pcbc  12492  ctinf  12590  nninfdc  12613  isnsgrp  12992  issubmnd  13026  nmzsubg  13283  ghmnsgima  13341  srg1zr  13486  ring1eq0  13547  mulgass2  13557  rhmdvdsr  13674  rmodislmod  13850  topssnei  14341  cnptopco  14401  cnconst2  14412  cnptoprest  14418  cnpdis  14421  upxp  14451  bldisj  14580  blgt0  14581  bl2in  14582  blss2ps  14585  blss2  14586  xblm  14596  blssps  14606  blss  14607  xmetresbl  14619  bdbl  14682  bdmopn  14683  metcnp3  14690  metcnp  14691  metcnp2  14692  dvfvalap  14860  dvcnp2cntop  14878  dvcn  14879  ply1term  14922  dvply1  14943  logdivlti  15057  ltexp2  15115  lgsfvalg  15162  lgsneg  15181  lgsdilem  15184  lgsdirprm  15191  lgsdir  15192  lgsdi  15194  lgsne0  15195  1dom1el  15553