Theorem simp3rl 1226

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

Assertion

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

Proof of Theorem simp3rl

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

Syntax hints:   → wi 4   ∧ wa 387   ∧ w3a 1068

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 199  df-an 388  df-3an 1070

This theorem is referenced by:  omeu  8012  hashbclem  13623  ntrivcvgmul  15118  tsmsxp  22466  tgqioo  23111  ovolunlem2  23802  plyadd  24510  plymul  24511  coeeu  24518  tghilberti2  26126  cvmlift2lem10  32141  nosupbnd1lem2  32727  btwnconn1lem1  33066  btwnconn1lem2  33067  btwnconn1lem12  33077  lplnexllnN  36142  2llnjN  36145  4atlem12b  36189  lplncvrlvol2  36193  lncmp  36361  cdlema2N  36370  cdlemc2  36770  cdleme11a  36838  cdleme22eALTN  36923  cdleme24  36930  cdleme27a  36945  cdleme27N  36947  cdleme28  36951  cdlemefs29bpre0N  36994  cdlemefs29bpre1N  36995  cdlemefs29cpre1N  36996  cdlemefs29clN  36997  cdlemefs32fvaN  37000  cdlemefs32fva1  37001  cdleme36m  37039  cdleme39a  37043  cdleme17d3  37074  cdleme50trn2  37129  cdlemg36  37292  cdlemj3  37401  cdlemkfid1N  37499  cdlemkid1  37500  cdlemk19ylem  37508  cdlemk19xlem  37520  dihlsscpre  37812  dihord4  37836  dihatlat  37912  mapdh9a  38367  jm2.27  38998