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  8552  hashbclem  14424  ntrivcvgmul  15875  tsmsxp  24049  tgqioo  24695  ovolunlem2  25406  plyadd  26129  plymul  26130  coeeu  26137  nosupbnd1lem2  27628  noinfbnd1lem2  27643  tghilberti2  28572  cvmlift2lem10  35306  btwnconn1lem1  36082  btwnconn1lem2  36083  btwnconn1lem12  36093  lplnexllnN  39565  2llnjN  39568  4atlem12b  39612  lplncvrlvol2  39616  lncmp  39784  cdlema2N  39793  cdlemc2  40193  cdleme11a  40261  cdleme22eALTN  40346  cdleme24  40353  cdleme27a  40368  cdleme27N  40370  cdleme28  40374  cdlemefs29bpre0N  40417  cdlemefs29bpre1N  40418  cdlemefs29cpre1N  40419  cdlemefs29clN  40420  cdlemefs32fvaN  40423  cdlemefs32fva1  40424  cdleme36m  40462  cdleme39a  40466  cdleme17d3  40497  cdleme50trn2  40552  cdlemg36  40715  cdlemj3  40824  cdlemkfid1N  40922  cdlemkid1  40923  cdlemk19ylem  40931  cdlemk19xlem  40943  dihlsscpre  41235  dihord4  41259  dihatlat  41335  mapdh9a  41790  jm2.27  43004