Theorem simp3rr 1244

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

Assertion

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

Proof of Theorem simp3rr

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

Syntax hints:   → wi 4   ∧ wa 399   ∧ w3a 1084

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 210  df-an 400  df-3an 1086

This theorem is referenced by:  omeu  8194  ntrivcvgmul  15250  tsmsxp  22760  tgqioo  23405  ovolunlem2  24102  plyadd  24814  plymul  24815  coeeu  24822  tghilberti2  26432  cvmlift2lem10  32672  nosupbnd1lem2  33322  btwnconn1lem1  33661  lplnexllnN  36860  2llnjN  36863  4atlem12b  36907  lplncvrlvol2  36911  lncmp  37079  cdlema2N  37088  cdleme11a  37556  cdleme24  37648  cdleme28  37669  cdlemefr29bpre0N  37702  cdlemefr29clN  37703  cdlemefr32fvaN  37705  cdlemefr32fva1  37706  cdlemefs29bpre0N  37712  cdlemefs29bpre1N  37713  cdlemefs29cpre1N  37714  cdlemefs29clN  37715  cdlemefs32fvaN  37718  cdlemefs32fva1  37719  cdleme36m  37757  cdleme17d3  37792  cdlemg36  38010  cdlemj3  38119  cdlemkid1  38218  cdlemk19ylem  38226  cdlemk19xlem  38238  dihlsscpre  38530  dihord4  38554  dihmeetlem1N  38586  dihatlat  38630  jm2.27  39949