Theorem simp3rl 1313

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

Assertion

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

Proof of Theorem simp3rl

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

Syntax hints:   → wi 4   ∧ wa 383   ∧ w3a 1072

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 197  df-an 385  df-3an 1074

This theorem is referenced by:  omeu  7834  hashbclem  13428  ntrivcvgmul  14833  tsmsxp  22159  tgqioo  22804  ovolunlem2  23466  plyadd  24172  plymul  24173  coeeu  24180  tghilberti2  25732  cvmlift2lem10  31601  nosupbnd1lem2  32161  btwnconn1lem1  32500  btwnconn1lem2  32501  btwnconn1lem12  32511  lplnexllnN  35353  2llnjN  35356  4atlem12b  35400  lplncvrlvol2  35404  lncmp  35572  cdlema2N  35581  cdlemc2  35982  cdleme11a  36050  cdleme22eALTN  36135  cdleme24  36142  cdleme27a  36157  cdleme27N  36159  cdleme28  36163  cdlemefs29bpre0N  36206  cdlemefs29bpre1N  36207  cdlemefs29cpre1N  36208  cdlemefs29clN  36209  cdlemefs32fvaN  36212  cdlemefs32fva1  36213  cdleme36m  36251  cdleme39a  36255  cdleme17d3  36286  cdleme50trn2  36341  cdlemg36  36504  cdlemj3  36613  cdlemkfid1N  36711  cdlemkid1  36712  cdlemk19ylem  36720  cdlemk19xlem  36732  dihlsscpre  37025  dihord4  37049  dihatlat  37125  mapdh9a  37581  jm2.27  38077