Theorem simp3rl 1243

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

Assertion

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

Proof of Theorem simp3rl

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

Syntax hints:   → wi 4   ∧ wa 394   ∧ 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 206  df-an 395  df-3an 1086

This theorem is referenced by:  omeu  8619  hashbclem  14475  ntrivcvgmul  15919  tsmsxp  24150  tgqioo  24807  ovolunlem2  25518  plyadd  26241  plymul  26242  coeeu  26249  nosupbnd1lem2  27736  noinfbnd1lem2  27751  tghilberti2  28607  cvmlift2lem10  35225  btwnconn1lem1  35996  btwnconn1lem2  35997  btwnconn1lem12  36007  lplnexllnN  39348  2llnjN  39351  4atlem12b  39395  lplncvrlvol2  39399  lncmp  39567  cdlema2N  39576  cdlemc2  39976  cdleme11a  40044  cdleme22eALTN  40129  cdleme24  40136  cdleme27a  40151  cdleme27N  40153  cdleme28  40157  cdlemefs29bpre0N  40200  cdlemefs29bpre1N  40201  cdlemefs29cpre1N  40202  cdlemefs29clN  40203  cdlemefs32fvaN  40206  cdlemefs32fva1  40207  cdleme36m  40245  cdleme39a  40249  cdleme17d3  40280  cdleme50trn2  40335  cdlemg36  40498  cdlemj3  40607  cdlemkfid1N  40705  cdlemkid1  40706  cdlemk19ylem  40714  cdlemk19xlem  40726  dihlsscpre  41018  dihord4  41042  dihatlat  41118  mapdh9a  41573  jm2.27  42778