Theorem simp3rr 1266

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

Assertion

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

Proof of Theorem simp3rr

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∧ w3a 1103

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105

This theorem is used by:  poxp3  8151  omeu  8577  ntrivcvgmul  16051  tsmsxp  24454  tgqioo  25099  ovolunlem2  25799  plyadd  26516  plymul  26517  coeeu  26524  nosupbnd1lem2  28048  noinfbnd1lem2  28063  tghilberti2  29088  cvmlift2lem10  36046  btwnconn1lem1  36822  lplnexllnN  40589  2llnjN  40592  4atlem12b  40636  lplncvrlvol2  40640  lncmp  40808  cdlema2N  40817  cdleme11a  41285  cdleme24  41377  cdleme28  41398  cdlemefr29bpre0N  41431  cdlemefr29clN  41432  cdlemefr32fvaN  41434  cdlemefr32fva1  41435  cdlemefs29bpre0N  41441  cdlemefs29bpre1N  41442  cdlemefs29cpre1N  41443  cdlemefs29clN  41444  cdlemefs32fvaN  41447  cdlemefs32fva1  41448  cdleme36m  41486  cdleme17d3  41521  cdlemg36  41739  cdlemj3  41848  cdlemkid1  41947  cdlemk19ylem  41955  cdlemk19xlem  41967  dihlsscpre  42259  dihord4  42283  dihmeetlem1N  42315  dihatlat  42359  jm2.27  43968