Theorem simp3rl 1253

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

Assertion

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

Proof of Theorem simp3rl

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

Syntax hints:   → wi 4   ∧ wa 396   ∧ w3a 1092

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 208  df-an 397  df-3an 1094

This theorem is referenced by:  omeu  8517  hashbclem  14412  ntrivcvgmul  15865  tsmsxp  24145  tgqioo  24790  ovolunlem2  25490  plyadd  26207  plymul  26208  coeeu  26215  nosupbnd1lem2  27698  noinfbnd1lem2  27713  tghilberti2  28731  cvmlift2lem10  35547  btwnconn1lem1  36322  btwnconn1lem2  36323  btwnconn1lem12  36333  lplnexllnN  40063  2llnjN  40066  4atlem12b  40110  lplncvrlvol2  40114  lncmp  40282  cdlema2N  40291  cdlemc2  40691  cdleme11a  40759  cdleme22eALTN  40844  cdleme24  40851  cdleme27a  40866  cdleme27N  40868  cdleme28  40872  cdlemefs29bpre0N  40915  cdlemefs29bpre1N  40916  cdlemefs29cpre1N  40917  cdlemefs29clN  40918  cdlemefs32fvaN  40921  cdlemefs32fva1  40922  cdleme36m  40960  cdleme39a  40964  cdleme17d3  40995  cdleme50trn2  41050  cdlemg36  41213  cdlemj3  41322  cdlemkfid1N  41420  cdlemkid1  41421  cdlemk19ylem  41429  cdlemk19xlem  41441  dihlsscpre  41733  dihord4  41757  dihatlat  41833  mapdh9a  42288  jm2.27  43460