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  7220  smo11  8306  zsupss  12862  lsmcv  21108  lspsolvlem  21109  mat2pmatghm  22686  mat2pmatmul  22687  plyadd  26190  plymul  26191  coeeu  26198  aannenlem1  26304  logexprlim  27204  ax5seglem6  29019  ax5seg  29023  mdetpmtr1  34000  mdetpmtr2  34001  wsuclem  36036  btwnconn1lem2  36301  btwnconn1lem3  36302  btwnconn1lem4  36303  btwnconn1lem12  36311  lshpsmreu  39482  2llnmat  39897  lvolex3N  39911  lnjatN  40153  pclfinclN  40323  lhpat3  40419  cdlemd6  40576  cdlemfnid  40937  cdlemk19ylem  41303  dihlsscpre  41607  dih1dimb2  41614  dihglblem6  41713  pellex  43189  tfsconcatrn  43696  mullimc  45973  mullimcf  45980  limcperiod  45985  cncfshift  46229  cncfperiod  46234