Theorem simp3rl 1244

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

Assertion

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

Proof of Theorem simp3rl

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

Syntax hints:   → wi 4   ∧ wa 394   ∧ w3a 1085

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 1087

This theorem is referenced by:  omeu  8587  hashbclem  14415  ntrivcvgmul  15852  tsmsxp  23879  tgqioo  24536  ovolunlem2  25247  plyadd  25966  plymul  25967  coeeu  25974  nosupbnd1lem2  27448  noinfbnd1lem2  27463  tghilberti2  28156  cvmlift2lem10  34601  btwnconn1lem1  35363  btwnconn1lem2  35364  btwnconn1lem12  35374  lplnexllnN  38738  2llnjN  38741  4atlem12b  38785  lplncvrlvol2  38789  lncmp  38957  cdlema2N  38966  cdlemc2  39366  cdleme11a  39434  cdleme22eALTN  39519  cdleme24  39526  cdleme27a  39541  cdleme27N  39543  cdleme28  39547  cdlemefs29bpre0N  39590  cdlemefs29bpre1N  39591  cdlemefs29cpre1N  39592  cdlemefs29clN  39593  cdlemefs32fvaN  39596  cdlemefs32fva1  39597  cdleme36m  39635  cdleme39a  39639  cdleme17d3  39670  cdleme50trn2  39725  cdlemg36  39888  cdlemj3  39997  cdlemkfid1N  40095  cdlemkid1  40096  cdlemk19ylem  40104  cdlemk19xlem  40116  dihlsscpre  40408  dihord4  40432  dihatlat  40508  mapdh9a  40963  jm2.27  42049