Theorem simp1rl 1257

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

Assertion

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

Proof of Theorem simp1rl

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∧ w3a 1103

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105

This theorem is used by:  f1imass  7269  smo11  8360  zsupss  12979  lsmcv  21302  lspsolvlem  21303  mat2pmatghm  22924  mat2pmatmul  22925  plyadd  26411  plymul  26412  coeeu  26419  aannenlem1  26528  logexprlim  27426  ax5seglem6  29321  ax5seg  29325  mdetpmtr1  34244  mdetpmtr2  34245  wsuclem  36336  btwnconn1lem2  36601  btwnconn1lem3  36602  btwnconn1lem4  36603  btwnconn1lem12  36611  lshpsmreu  39924  2llnmat  40339  lvolex3N  40353  lnjatN  40595  pclfinclN  40765  lhpat3  40861  cdlemd6  41018  cdlemfnid  41379  cdlemk19ylem  41745  dihlsscpre  42049  dih1dimb2  42056  dihglblem6  42155  pellex  43603  tfsconcatrn  44110  mullimc  46373  mullimcf  46380  limcperiod  46385  cncfshift  46629  cncfperiod  46634  nprmmul2  48318