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  8572  hashbclem  14502  ntrivcvgmul  15974  tsmsxp  24341  tgqioo  24986  ovolunlem2  25686  plyadd  26403  plymul  26404  coeeu  26411  nosupbnd1lem2  27902  noinfbnd1lem2  27917  tghilberti2  28940  cvmlift2lem10  35817  btwnconn1lem1  36592  btwnconn1lem2  36593  btwnconn1lem12  36603  lplnexllnN  40371  2llnjN  40374  4atlem12b  40418  lplncvrlvol2  40422  lncmp  40590  cdlema2N  40599  cdlemc2  40999  cdleme11a  41067  cdleme22eALTN  41152  cdleme24  41159  cdleme27a  41174  cdleme27N  41176  cdleme28  41180  cdlemefs29bpre0N  41223  cdlemefs29bpre1N  41224  cdlemefs29cpre1N  41225  cdlemefs29clN  41226  cdlemefs32fvaN  41229  cdlemefs32fva1  41230  cdleme36m  41268  cdleme39a  41272  cdleme17d3  41303  cdleme50trn2  41358  cdlemg36  41521  cdlemj3  41630  cdlemkfid1N  41728  cdlemkid1  41729  cdlemk19ylem  41737  cdlemk19xlem  41749  dihlsscpre  42041  dihord4  42065  dihatlat  42141  mapdh9a  42596  jm2.27  43768