Theorem simp1rl 1236

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

Assertion

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

Proof of Theorem simp1rl

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

Syntax hints:   → wi 4   ∧ wa 394   ∧ w3a 1085

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 206  df-an 395  df-3an 1087

This theorem is referenced by:  f1imass  7265  smo11  8366  zsupss  12925  lsmcv  20899  lspsolvlem  20900  mat2pmatghm  22452  mat2pmatmul  22453  plyadd  25966  plymul  25967  coeeu  25974  aannenlem1  26077  logexprlim  26964  ax5seglem6  28459  ax5seg  28463  mdetpmtr1  33101  mdetpmtr2  33102  wsuclem  35101  btwnconn1lem2  35364  btwnconn1lem3  35365  btwnconn1lem4  35366  btwnconn1lem12  35374  lshpsmreu  38282  2llnmat  38698  lvolex3N  38712  lnjatN  38954  pclfinclN  39124  lhpat3  39220  cdlemd6  39377  cdlemfnid  39738  cdlemk19ylem  40104  dihlsscpre  40408  dih1dimb2  40415  dihglblem6  40514  pellex  41875  tfsconcatrn  42394  mullimc  44630  mullimcf  44637  limcperiod  44642  cncfshift  44888  cncfperiod  44893