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  7294  smo11  8403  zsupss  13094  lsmcv  21452  lspsolvlem  21453  mat2pmatghm  23081  mat2pmatmul  23082  plyadd  26569  plymul  26570  coeeu  26577  aannenlem1  26688  logexprlim  27585  ax5seglem6  29545  ax5seg  29549  mdetpmtr1  34538  mdetpmtr2  34539  wsuclem  36778  btwnconn1lem2  37044  btwnconn1lem3  37045  btwnconn1lem4  37046  btwnconn1lem12  37054  lshpsmreu  40369  2llnmat  40784  lvolex3N  40798  lnjatN  41040  pclfinclN  41210  lhpat3  41306  cdlemd6  41463  cdlemfnid  41824  cdlemk19ylem  42190  dihlsscpre  42494  dih1dimb2  42501  dihglblem6  42600  pellex  44046  tfsconcatrn  44547  mullimc  46843  mullimcf  46850  limcperiod  46855  cncfshift  47099  cncfperiod  47104  nprmmul2  48825