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  8500  hashbclem  14359  ntrivcvgmul  15809  tsmsxp  24071  tgqioo  24716  ovolunlem2  25427  plyadd  26150  plymul  26151  coeeu  26158  nosupbnd1lem2  27649  noinfbnd1lem2  27664  tghilberti2  28617  cvmlift2lem10  35354  btwnconn1lem1  36127  btwnconn1lem2  36128  btwnconn1lem12  36138  lplnexllnN  39609  2llnjN  39612  4atlem12b  39656  lplncvrlvol2  39660  lncmp  39828  cdlema2N  39837  cdlemc2  40237  cdleme11a  40305  cdleme22eALTN  40390  cdleme24  40397  cdleme27a  40412  cdleme27N  40414  cdleme28  40418  cdlemefs29bpre0N  40461  cdlemefs29bpre1N  40462  cdlemefs29cpre1N  40463  cdlemefs29clN  40464  cdlemefs32fvaN  40467  cdlemefs32fva1  40468  cdleme36m  40506  cdleme39a  40510  cdleme17d3  40541  cdleme50trn2  40596  cdlemg36  40759  cdlemj3  40868  cdlemkfid1N  40966  cdlemkid1  40967  cdlemk19ylem  40975  cdlemk19xlem  40987  dihlsscpre  41279  dihord4  41303  dihatlat  41379  mapdh9a  41834  jm2.27  43047