Theorem simp3lr 1245

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

Assertion

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

Proof of Theorem simp3lr

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

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

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 1089

This theorem is referenced by:  f1oiso2  7388  omeu  8641  ntrivcvgmul  15950  tsmsxp  24184  tgqioo  24841  ovolunlem2  25552  plyadd  26276  plymul  26277  coeeu  26284  nosupbnd1lem2  27772  noinfbnd1lem2  27787  tghilberti2  28664  btwnconn1lem2  36052  btwnconn1lem3  36053  btwnconn1lem4  36054  athgt  39413  2llnjN  39524  4atlem12b  39568  lncmp  39740  cdlema2N  39749  cdleme21ct  40286  cdleme24  40309  cdleme27a  40324  cdleme28  40330  cdleme42b  40435  cdlemf  40520  dihlsscpre  41191  dihord4  41215  dihord5apre  41219  pellex  42791  jm2.27  42965