Theorem simp3lr 1246

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 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:  f1oiso2  7286  omeu  8500  ntrivcvgmul  15806  tsmsxp  24068  tgqioo  24713  ovolunlem2  25424  plyadd  26147  plymul  26148  coeeu  26155  nosupbnd1lem2  27646  noinfbnd1lem2  27661  tghilberti2  28614  btwnconn1lem2  36121  btwnconn1lem3  36122  btwnconn1lem4  36123  athgt  39494  2llnjN  39605  4atlem12b  39649  lncmp  39821  cdlema2N  39830  cdleme21ct  40367  cdleme24  40390  cdleme27a  40405  cdleme28  40411  cdleme42b  40516  cdlemf  40601  dihlsscpre  41272  dihord4  41296  dihord5apre  41300  pellex  42867  jm2.27  43040