Theorem simpl2 1025

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

Assertion

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

Proof of Theorem simpl2

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

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

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 1004

This theorem is referenced by:  simpll2  1061  simprl2  1067  simp1l2  1115  simp2l2  1121  simp3l2  1127  3anandirs  1382  rspc3ev  2924  ifnetruedc  3646  tfisi  4680  brcogw  4894  oawordi  6628  nnmord  6676  nnmword  6677  ac6sfi  7073  unsnfi  7097  unsnfidcel  7099  ordiso2  7218  prarloclemarch2  7622  enq0tr  7637  distrlem4prl  7787  distrlem4pru  7788  ltaprg  7822  aptiprlemu  7843  lelttr  8251  ltletr  8252  readdcan  8302  addcan  8342  addcan2  8343  ltadd2  8582  ltmul1a  8754  ltmul1  8755  divmulassap  8858  divmulasscomap  8859  lemul1a  9021  xrlelttr  10019  xrltletr  10020  xaddass  10082  xleadd1a  10086  xltadd1  10089  xlesubadd  10096  ixxdisj  10116  icoshftf1o  10204  icodisj  10205  lincmb01cmp  10216  iccf1o  10217  fztri3or  10252  ioom  10497  modqmuladdim  10606  modqmuladdnn0  10607  q2submod  10624  modqaddmulmod  10630  seqp1g  10705  exp3val  10780  ltexp2a  10830  exple1  10834  expnbnd  10902  expnlbnd2  10904  nn0ltexp2  10948  nn0leexp2  10949  mulsubdivbinom2ap  10950  expcan  10955  fiprsshashgt1  11057  fun2dmnop0  11087  ccatass  11161  fzowrddc  11200  swrdclg  11203  ccatopth  11269  pfxccatin12lem2a  11280  maxleastb  11746  maxltsup  11750  xrltmaxsup  11789  xrmaxltsup  11790  xrmaxaddlem  11792  xrmaxadd  11793  addcn2  11842  mulcn2  11844  geoisum1c  12052  dvdsval2  12322  dvdsmodexp  12327  dvdsadd2b  12372  dvdsaddre2b  12373  dvdsmod  12394  oexpneg  12409  divalglemex  12454  divalg  12456  gcdass  12557  rplpwr  12569  rppwr  12570  nnminle  12577  lcmass  12628  coprmdvds2  12636  rpmulgcd2  12638  rpdvds  12642  cncongr2  12647  rpexp  12696  znege1  12721  prmdiveq  12779  hashgcdlem  12781  odzdvds  12789  coprimeprodsq2  12802  pythagtriplem3  12811  pythagtriplem4  12812  pcdvdsb  12864  pcbc  12895  ctinf  13022  nninfdc  13045  isnsgrp  13460  issubmnd  13496  nmzsubg  13768  ghmnsgima  13826  srg1zr  13971  ring1eq0  14032  mulgass2  14042  rhmdvdsr  14160  rmodislmod  14336  topssnei  14857  cnptopco  14917  cnconst2  14928  cnptoprest  14934  cnpdis  14937  upxp  14967  bldisj  15096  blgt0  15097  bl2in  15098  blss2ps  15101  blss2  15102  xblm  15112  blssps  15122  blss  15123  xmetresbl  15135  bdbl  15198  bdmopn  15199  metcnp3  15206  metcnp  15207  metcnp2  15208  dvfvalap  15376  dvcnp2cntop  15394  dvcn  15395  ply1term  15438  dvply1  15460  logdivlti  15576  ltexp2  15636  lgsfvalg  15705  lgsneg  15724  lgsdilem  15727  lgsdirprm  15734  lgsdir  15735  lgsdi  15737  lgsne0  15738  1dom1el  16463