Theorem simpl2 1032

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

Assertion

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

Proof of Theorem simpl2

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

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

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 1011

This theorem is referenced by:  simpll2  1068  simprl2  1074  simp1l2  1122  simp2l2  1128  simp3l2  1134  3anandirs  1389  rspc3ev  2947  ifnetruedc  3684  tfisi  4732  brcogw  4947  oawordi  6736  nnmord  6784  nnmword  6785  1dom1el  7101  mapunen  7145  ac6sfi  7196  unsnfi  7220  unsnfidcel  7222  ordiso2  7369  prarloclemarch2  7780  enq0tr  7795  distrlem4prl  7945  distrlem4pru  7946  ltaprg  7980  aptiprlemu  8001  lelttr  8408  ltletr  8409  readdcan  8460  addcan  8500  addcan2  8501  ltadd2  8741  ltmul1a  8913  ltmul1  8914  divmulassap  9019  divmulasscomap  9020  lemul1a  9182  xrlelttr  10191  xrltletr  10192  xaddass  10254  xleadd1a  10258  xltadd1  10261  xlesubadd  10268  ixxdisj  10288  icoshftf1o  10376  icodisj  10377  lincmb01cmp  10388  lincmble  10389  iccf1o  10390  fztri3or  10426  ioom  10678  modqmuladdim  10787  modqmuladdnn0  10788  q2submod  10805  modqaddmulmod  10811  seqp1g  10886  exp3val  10961  ltexp2a  11011  exple1  11015  expnbnd  11084  expnlbnd2  11086  nn0ltexp2  11130  nn0leexp2  11131  mulsubdivbinom2ap  11132  expcan  11137  fiprsshashgt1  11241  hashtpgim  11280  hashtpg  11282  fun2dmnop0  11285  ccatass  11359  fzowrddc  11402  swrdclg  11405  ccatopth  11471  pfxccatin12lem2a  11482  maxleastb  11963  maxltsup  11967  xrltmaxsup  12006  xrmaxltsup  12007  xrmaxaddlem  12009  xrmaxadd  12010  addcn2  12059  mulcn2  12061  geoisum1c  12270  dvdsval2  12540  dvdsmodexp  12545  dvdsadd2b  12590  dvdsaddre2b  12591  dvdsmod  12612  oexpneg  12627  divalglemex  12672  divalg  12674  gcdass  12775  rplpwr  12787  rppwr  12788  nnminle  12795  lcmass  12846  coprmdvds2  12854  rpmulgcd2  12856  rpdvds  12860  cncongr2  12865  rpexp  12914  znege1  12939  prmdiveq  12997  hashgcdlem  12999  odzdvds  13007  coprimeprodsq2  13020  pythagtriplem3  13029  pythagtriplem4  13030  pcdvdsb  13082  pcbc  13113  ctinf  13304  nninfdc  13327  isnsgrp  13704  issubmnd  13738  nmzsubg  13996  ghmnsgima  14054  ring1eq0  14336  mulgass2  14346  rhmdvdsr  14465  rmodislmod  14671  issubassa  14996  topssnei  15246  cnptopco  15306  cnconst2  15317  cnptoprest  15323  cnpdis  15326  upxp  15356  bldisj  15485  blgt0  15486  bl2in  15487  blss2ps  15490  blss2  15491  xblm  15501  blssps  15511  blss  15512  xmetresbl  15524  bdbl  15587  bdmopn  15588  metcnp3  15595  metcnp  15596  metcnp2  15597  dvfvalap  15765  dvcnp2cntop  15783  dvcn  15784  ply1term  15827  dvply1  15849  logdivlti  15965  ltexp2  16026  pellexlem2  16075  lgsfvalg  16107  lgsneg  16126  lgsdilem  16129  lgsdirprm  16136  lgsdir  16137  lgsdi  16139  lgsne0  16140  clwwlknonex2e  16664