Theorem simp3rl 1247

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

Assertion

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

Proof of Theorem simp3rl

Step	Hyp	Ref	Expression
1		simprl 770	. 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:  omeu  8506  hashbclem  14365  ntrivcvgmul  15815  tsmsxp  24076  tgqioo  24721  ovolunlem2  25432  plyadd  26155  plymul  26156  coeeu  26163  nosupbnd1lem2  27654  noinfbnd1lem2  27669  tghilberti2  28622  cvmlift2lem10  35363  btwnconn1lem1  36138  btwnconn1lem2  36139  btwnconn1lem12  36149  lplnexllnN  39669  2llnjN  39672  4atlem12b  39716  lplncvrlvol2  39720  lncmp  39888  cdlema2N  39897  cdlemc2  40297  cdleme11a  40365  cdleme22eALTN  40450  cdleme24  40457  cdleme27a  40472  cdleme27N  40474  cdleme28  40478  cdlemefs29bpre0N  40521  cdlemefs29bpre1N  40522  cdlemefs29cpre1N  40523  cdlemefs29clN  40524  cdlemefs32fvaN  40527  cdlemefs32fva1  40528  cdleme36m  40566  cdleme39a  40570  cdleme17d3  40601  cdleme50trn2  40656  cdlemg36  40819  cdlemj3  40928  cdlemkfid1N  41026  cdlemkid1  41027  cdlemk19ylem  41035  cdlemk19xlem  41047  dihlsscpre  41339  dihord4  41363  dihatlat  41439  mapdh9a  41894  jm2.27  43106