Theorem simp1lr 1238

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

Assertion

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

Proof of Theorem simp1lr

Step	Hyp	Ref	Expression
1		simplr 768	. 2 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜓)
2	1	3ad2ant1 1133	1 ⊢ ((((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ 𝜃 ∧ 𝜏) → 𝜓)

Syntax hints:   → wi 4   ∧ wa 395   ∧ w3a 1086

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 1088

This theorem is referenced by:  lspsolvlem  21059  dmatcrng  22396  scmatcrng  22415  1marepvsma1  22477  mdetunilem7  22512  mat2pmatghm  22624  pmatcollpwscmatlem2  22684  mp2pm2mplem4  22703  ax5seg  28872  measinblem  34217  btwnconn1lem13  36094  athgt  39457  llnle  39519  lplnle  39541  lhpexle1  40009  lhpat3  40047  tendoicl  40797  cdlemk55b  40961  pellex  42830  ssfiunibd  45314  mullimc  45621  mullimcf  45628  icccncfext  45892  etransclem32  46271  uhgrimisgrgriclem  47934