Theorem simp1rl 1240

Description: Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)

Assertion

Ref	Expression
simp1rl	⊢ (((𝜒 ∧ (𝜑 ∧ 𝜓)) ∧ 𝜃 ∧ 𝜏) → 𝜑)

Proof of Theorem simp1rl

Step	Hyp	Ref	Expression
1		simprl 771	. 2 ⊢ ((𝜒 ∧ (𝜑 ∧ 𝜓)) → 𝜑)
2	1	3ad2ant1 1134	1 ⊢ (((𝜒 ∧ (𝜑 ∧ 𝜓)) ∧ 𝜃 ∧ 𝜏) → 𝜑)

Syntax hints:   → wi 4   ∧ wa 395   ∧ w3a 1087

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 207  df-an 396  df-3an 1089

This theorem is referenced by:  f1imass  7219  smo11  8304  zsupss  12887  lsmcv  21139  lspsolvlem  21140  mat2pmatghm  22695  mat2pmatmul  22696  plyadd  26182  plymul  26183  coeeu  26190  aannenlem1  26294  logexprlim  27188  ax5seglem6  29003  ax5seg  29007  mdetpmtr1  33967  mdetpmtr2  33968  wsuclem  36005  btwnconn1lem2  36270  btwnconn1lem3  36271  btwnconn1lem4  36272  btwnconn1lem12  36280  lshpsmreu  39555  2llnmat  39970  lvolex3N  39984  lnjatN  40226  pclfinclN  40396  lhpat3  40492  cdlemd6  40649  cdlemfnid  41010  cdlemk19ylem  41376  dihlsscpre  41680  dih1dimb2  41687  dihglblem6  41786  pellex  43263  tfsconcatrn  43770  mullimc  46046  mullimcf  46053  limcperiod  46058  cncfshift  46302  cncfperiod  46307  nprmmul2  47988