Theorem simp3lr 1247

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

Assertion

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

Proof of Theorem simp3lr

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

Syntax hints:   → wi 4   ∧ wa 399   ∧ w3a 1089

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 210  df-an 400  df-3an 1091

This theorem is referenced by:  f1oiso2  7139  omeu  8291  ntrivcvgmul  15429  tsmsxp  23006  tgqioo  23651  ovolunlem2  24349  plyadd  25065  plymul  25066  coeeu  25073  tghilberti2  26683  nosupbnd1lem2  33598  noinfbnd1lem2  33613  btwnconn1lem2  34076  btwnconn1lem3  34077  btwnconn1lem4  34078  athgt  37156  2llnjN  37267  4atlem12b  37311  lncmp  37483  cdlema2N  37492  cdleme21ct  38029  cdleme24  38052  cdleme27a  38067  cdleme28  38073  cdleme42b  38178  cdlemf  38263  dihlsscpre  38934  dihord4  38958  dihord5apre  38962  pellex  40301  jm2.27  40474