Theorem simp3rl 1263

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

Assertion

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

Proof of Theorem simp3rl

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

Syntax hints:   → wi 4   ∧ wa 400   ∧ w3a 1101

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 210  df-an 401  df-3an 1103

This theorem is referenced by:  omeu  8558  hashbclem  14477  ntrivcvgmul  15944  tsmsxp  24269  tgqioo  24914  ovolunlem2  25614  plyadd  26331  plymul  26332  coeeu  26339  nosupbnd1lem2  27827  noinfbnd1lem2  27842  tghilberti2  28861  cvmlift2lem10  35670  btwnconn1lem1  36445  btwnconn1lem2  36446  btwnconn1lem12  36456  lplnexllnN  40195  2llnjN  40198  4atlem12b  40242  lplncvrlvol2  40246  lncmp  40414  cdlema2N  40423  cdlemc2  40823  cdleme11a  40891  cdleme22eALTN  40976  cdleme24  40983  cdleme27a  40998  cdleme27N  41000  cdleme28  41004  cdlemefs29bpre0N  41047  cdlemefs29bpre1N  41048  cdlemefs29cpre1N  41049  cdlemefs29clN  41050  cdlemefs32fvaN  41053  cdlemefs32fva1  41054  cdleme36m  41092  cdleme39a  41096  cdleme17d3  41127  cdleme50trn2  41182  cdlemg36  41345  cdlemj3  41454  cdlemkfid1N  41552  cdlemkid1  41553  cdlemk19ylem  41561  cdlemk19xlem  41573  dihlsscpre  41865  dihord4  41889  dihatlat  41965  mapdh9a  42420  jm2.27  43592