Theorem simp3rr 1314

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

Assertion

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

Proof of Theorem simp3rr

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

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

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 1074

This theorem is referenced by:  omeu  7836  ntrivcvgmul  14853  tsmsxp  22179  tgqioo  22824  ovolunlem2  23486  plyadd  24192  plymul  24193  coeeu  24200  tghilberti2  25753  cvmlift2lem10  31622  nosupbnd1lem2  32182  btwnconn1lem1  32521  lplnexllnN  35371  2llnjN  35374  4atlem12b  35418  lplncvrlvol2  35422  lncmp  35590  cdlema2N  35599  cdleme11a  36068  cdleme24  36160  cdleme28  36181  cdlemefr29bpre0N  36214  cdlemefr29clN  36215  cdlemefr32fvaN  36217  cdlemefr32fva1  36218  cdlemefs29bpre0N  36224  cdlemefs29bpre1N  36225  cdlemefs29cpre1N  36226  cdlemefs29clN  36227  cdlemefs32fvaN  36230  cdlemefs32fva1  36231  cdleme36m  36269  cdleme17d3  36304  cdlemg36  36522  cdlemj3  36631  cdlemkid1  36730  cdlemk19ylem  36738  cdlemk19xlem  36750  dihlsscpre  37043  dihord4  37067  dihmeetlem1N  37099  dihatlat  37143  jm2.27  38095