Theorem simp3lr 1264

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

Assertion

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

Proof of Theorem simp3lr

Step	Hyp	Ref	Expression
1		simplr 781	. 2 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜓)
2	1	3ad2ant3 1153	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:  f1oiso2  7352  omeu  8577  ntrivcvgmul  16051  tsmsxp  24454  tgqioo  25099  ovolunlem2  25799  plyadd  26516  plymul  26517  coeeu  26524  nosupbnd1lem2  28048  noinfbnd1lem2  28063  tghilberti2  29088  btwnconn1lem2  36823  btwnconn1lem3  36824  btwnconn1lem4  36825  athgt  40481  2llnjN  40592  4atlem12b  40636  lncmp  40808  cdlema2N  40817  cdleme21ct  41354  cdleme24  41377  cdleme27a  41392  cdleme28  41398  cdleme42b  41503  cdlemf  41588  dihlsscpre  42259  dihord4  42283  dihord5apre  42287  pellex  43795  jm2.27  43968