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  8512  hashbclem  14375  ntrivcvgmul  15825  tsmsxp  24099  tgqioo  24744  ovolunlem2  25455  plyadd  26178  plymul  26179  coeeu  26186  nosupbnd1lem2  27677  noinfbnd1lem2  27692  tghilberti2  28710  cvmlift2lem10  35506  btwnconn1lem1  36281  btwnconn1lem2  36282  btwnconn1lem12  36292  lplnexllnN  39824  2llnjN  39827  4atlem12b  39871  lplncvrlvol2  39875  lncmp  40043  cdlema2N  40052  cdlemc2  40452  cdleme11a  40520  cdleme22eALTN  40605  cdleme24  40612  cdleme27a  40627  cdleme27N  40629  cdleme28  40633  cdlemefs29bpre0N  40676  cdlemefs29bpre1N  40677  cdlemefs29cpre1N  40678  cdlemefs29clN  40679  cdlemefs32fvaN  40682  cdlemefs32fva1  40683  cdleme36m  40721  cdleme39a  40725  cdleme17d3  40756  cdleme50trn2  40811  cdlemg36  40974  cdlemj3  41083  cdlemkfid1N  41181  cdlemkid1  41182  cdlemk19ylem  41190  cdlemk19xlem  41202  dihlsscpre  41494  dihord4  41518  dihatlat  41594  mapdh9a  42049  jm2.27  43250