Theorem simp3rl 1265

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

Assertion

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

Proof of Theorem simp3rl

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∧ w3a 1103

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105

This theorem is used by:  omeu  8597  hashbclem  14601  ntrivcvgmul  16077  tsmsxp  24480  tgqioo  25125  ovolunlem2  25825  plyadd  26542  plymul  26543  coeeu  26550  nosupbnd1lem2  28072  noinfbnd1lem2  28087  tghilberti2  29112  cvmlift2lem10  36164  btwnconn1lem1  36945  btwnconn1lem2  36946  btwnconn1lem12  36956  lplnexllnN  40715  2llnjN  40718  4atlem12b  40762  lplncvrlvol2  40766  lncmp  40934  cdlema2N  40943  cdlemc2  41343  cdleme11a  41411  cdleme22eALTN  41496  cdleme24  41503  cdleme27a  41518  cdleme27N  41520  cdleme28  41524  cdlemefs29bpre0N  41567  cdlemefs29bpre1N  41568  cdlemefs29cpre1N  41569  cdlemefs29clN  41570  cdlemefs32fvaN  41573  cdlemefs32fva1  41574  cdleme36m  41612  cdleme39a  41616  cdleme17d3  41647  cdleme50trn2  41702  cdlemg36  41865  cdlemj3  41974  cdlemkfid1N  42072  cdlemkid1  42073  cdlemk19ylem  42081  cdlemk19xlem  42093  dihlsscpre  42385  dihord4  42409  dihatlat  42485  mapdh9a  42940  jm2.27  44109