Theorem simp3rl 1248

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

Assertion

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

Proof of Theorem simp3rl

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

Syntax hints:   → wi 4   ∧ wa 395   ∧ w3a 1087

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 1089

This theorem is referenced by:  omeu  8522  hashbclem  14387  ntrivcvgmul  15837  tsmsxp  24111  tgqioo  24756  ovolunlem2  25467  plyadd  26190  plymul  26191  coeeu  26198  nosupbnd1lem2  27689  noinfbnd1lem2  27704  tghilberti2  28722  cvmlift2lem10  35525  btwnconn1lem1  36300  btwnconn1lem2  36301  btwnconn1lem12  36311  lplnexllnN  39937  2llnjN  39940  4atlem12b  39984  lplncvrlvol2  39988  lncmp  40156  cdlema2N  40165  cdlemc2  40565  cdleme11a  40633  cdleme22eALTN  40718  cdleme24  40725  cdleme27a  40740  cdleme27N  40742  cdleme28  40746  cdlemefs29bpre0N  40789  cdlemefs29bpre1N  40790  cdlemefs29cpre1N  40791  cdlemefs29clN  40792  cdlemefs32fvaN  40795  cdlemefs32fva1  40796  cdleme36m  40834  cdleme39a  40838  cdleme17d3  40869  cdleme50trn2  40924  cdlemg36  41087  cdlemj3  41196  cdlemkfid1N  41294  cdlemkid1  41295  cdlemk19ylem  41303  cdlemk19xlem  41315  dihlsscpre  41607  dihord4  41631  dihatlat  41707  mapdh9a  42162  jm2.27  43362