Theorem simp3rr 1155

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

Assertion

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

Proof of Theorem simp3rr

Step	Hyp	Ref	Expression
1		simprr 811	. 2 ⊢ ((𝜒 ∧ (𝜑 ∧ 𝜓)) → 𝜓)
2	1	3ad2ant3 1104	1 ⊢ ((𝜃 ∧ 𝜏 ∧ (𝜒 ∧ (𝜑 ∧ 𝜓))) → 𝜓)

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

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 197  df-an 385  df-3an 1056

This theorem is referenced by:  omeu  7710  ntrivcvgmul  14678  tsmsxp  22005  tgqioo  22650  ovolunlem2  23312  plyadd  24018  plymul  24019  coeeu  24026  tghilberti2  25578  cvmlift2lem10  31420  nosupbnd1lem2  31980  btwnconn1lem1  32319  lplnexllnN  35168  2llnjN  35171  4atlem12b  35215  lplncvrlvol2  35219  lncmp  35387  cdlema2N  35396  cdleme11a  35865  cdleme24  35957  cdleme28  35978  cdlemefr29bpre0N  36011  cdlemefr29clN  36012  cdlemefr32fvaN  36014  cdlemefr32fva1  36015  cdlemefs29bpre0N  36021  cdlemefs29bpre1N  36022  cdlemefs29cpre1N  36023  cdlemefs29clN  36024  cdlemefs32fvaN  36027  cdlemefs32fva1  36028  cdleme36m  36066  cdleme17d3  36101  cdlemg36  36319  cdlemj3  36428  cdlemkid1  36527  cdlemk19ylem  36535  cdlemk19xlem  36547  dihlsscpre  36840  dihord4  36864  dihmeetlem1N  36896  dihatlat  36940  jm2.27  37892