Theorem simp3lr 1126

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

Assertion

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

Proof of Theorem simp3lr

Step	Hyp	Ref	Expression
1		simplr 788	. 2 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜓)
2	1	3ad2ant3 1077	1 ⊢ ((𝜃 ∧ 𝜏 ∧ ((𝜑 ∧ 𝜓) ∧ 𝜒)) → 𝜓)

Syntax hints:   → wi 4   ∧ wa 383   ∧ w3a 1031

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 196  df-an 385  df-3an 1033

This theorem is referenced by:  f1oiso2  6502  omeu  7552  ntrivcvgmul  14473  tsmsxp  21768  tgqioo  22411  ovolunlem2  23073  plyadd  23777  plymul  23778  coeeu  23785  tghilberti2  25333  btwnconn1lem2  31365  btwnconn1lem3  31366  btwnconn1lem4  31367  athgt  33760  2llnjN  33871  4atlem12b  33915  lncmp  34087  cdlema2N  34096  cdleme21ct  34635  cdleme24  34658  cdleme27a  34673  cdleme28  34679  cdleme42b  34784  cdlemf  34869  dihlsscpre  35541  dihord4  35565  dihord5apre  35569  pellex  36417  jm2.27  36593