Theorem simp3rr 1248

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 1135	1 ⊢ ((𝜃 ∧ 𝜏 ∧ (𝜒 ∧ (𝜑 ∧ 𝜓))) → 𝜓)

Syntax hints:   → wi 4   ∧ wa 395   ∧ w3a 1086

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 207  df-an 396  df-3an 1088

This theorem is referenced by:  poxp3  8080  omeu  8500  ntrivcvgmul  15806  tsmsxp  24068  tgqioo  24713  ovolunlem2  25424  plyadd  26147  plymul  26148  coeeu  26155  nosupbnd1lem2  27646  noinfbnd1lem2  27661  tghilberti2  28614  cvmlift2lem10  35344  btwnconn1lem1  36120  lplnexllnN  39602  2llnjN  39605  4atlem12b  39649  lplncvrlvol2  39653  lncmp  39821  cdlema2N  39830  cdleme11a  40298  cdleme24  40390  cdleme28  40411  cdlemefr29bpre0N  40444  cdlemefr29clN  40445  cdlemefr32fvaN  40447  cdlemefr32fva1  40448  cdlemefs29bpre0N  40454  cdlemefs29bpre1N  40455  cdlemefs29cpre1N  40456  cdlemefs29clN  40457  cdlemefs32fvaN  40460  cdlemefs32fva1  40461  cdleme36m  40499  cdleme17d3  40534  cdlemg36  40752  cdlemj3  40861  cdlemkid1  40960  cdlemk19ylem  40968  cdlemk19xlem  40980  dihlsscpre  41272  dihord4  41296  dihmeetlem1N  41328  dihatlat  41372  jm2.27  43040