Theorem simp3rr 1133

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

Assertion

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

Proof of Theorem simp3rr

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

Syntax hints:   → wi 4   ∧ wa 384   ∧ w3a 1036

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 386  df-3an 1038

This theorem is referenced by:  omeu  7611  ntrivcvgmul  14554  tsmsxp  21863  tgqioo  22506  ovolunlem2  23168  plyadd  23872  plymul  23873  coeeu  23880  tghilberti2  25428  cvmlift2lem10  30994  btwnconn1lem1  31828  lplnexllnN  34316  2llnjN  34319  4atlem12b  34363  lplncvrlvol2  34367  lncmp  34535  cdlema2N  34544  cdleme11a  35013  cdleme24  35106  cdleme28  35127  cdlemefr29bpre0N  35160  cdlemefr29clN  35161  cdlemefr32fvaN  35163  cdlemefr32fva1  35164  cdlemefs29bpre0N  35170  cdlemefs29bpre1N  35171  cdlemefs29cpre1N  35172  cdlemefs29clN  35173  cdlemefs32fvaN  35176  cdlemefs32fva1  35177  cdleme36m  35215  cdleme17d3  35250  cdlemg36  35468  cdlemj3  35577  cdlemkid1  35676  cdlemk19ylem  35684  cdlemk19xlem  35696  dihlsscpre  35989  dihord4  36013  dihmeetlem1N  36045  dihatlat  36089  jm2.27  37041