Theorem simp3rr 1135

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

Assertion

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

Proof of Theorem simp3rr

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

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

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 1039

This theorem is referenced by:  omeu  7665  ntrivcvgmul  14634  tsmsxp  21958  tgqioo  22603  ovolunlem2  23266  plyadd  23973  plymul  23974  coeeu  23981  tghilberti2  25533  cvmlift2lem10  31294  nosupbnd1lem2  31855  btwnconn1lem1  32194  lplnexllnN  34850  2llnjN  34853  4atlem12b  34897  lplncvrlvol2  34901  lncmp  35069  cdlema2N  35078  cdleme11a  35547  cdleme24  35640  cdleme28  35661  cdlemefr29bpre0N  35694  cdlemefr29clN  35695  cdlemefr32fvaN  35697  cdlemefr32fva1  35698  cdlemefs29bpre0N  35704  cdlemefs29bpre1N  35705  cdlemefs29cpre1N  35706  cdlemefs29clN  35707  cdlemefs32fvaN  35710  cdlemefs32fva1  35711  cdleme36m  35749  cdleme17d3  35784  cdlemg36  36002  cdlemj3  36111  cdlemkid1  36210  cdlemk19ylem  36218  cdlemk19xlem  36230  dihlsscpre  36523  dihord4  36547  dihmeetlem1N  36579  dihatlat  36623  jm2.27  37575