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  7212  smo11  8297  zsupss  12878  lsmcv  21131  lspsolvlem  21132  mat2pmatghm  22705  mat2pmatmul  22706  plyadd  26192  plymul  26193  coeeu  26200  aannenlem1  26305  logexprlim  27202  ax5seglem6  29017  ax5seg  29021  mdetpmtr1  33983  mdetpmtr2  33984  wsuclem  36021  btwnconn1lem2  36286  btwnconn1lem3  36287  btwnconn1lem4  36288  btwnconn1lem12  36296  lshpsmreu  39569  2llnmat  39984  lvolex3N  39998  lnjatN  40240  pclfinclN  40410  lhpat3  40506  cdlemd6  40663  cdlemfnid  41024  cdlemk19ylem  41390  dihlsscpre  41694  dih1dimb2  41701  dihglblem6  41800  pellex  43281  tfsconcatrn  43788  mullimc  46064  mullimcf  46071  limcperiod  46076  cncfshift  46320  cncfperiod  46325  nprmmul2  48000