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  14517  ntrivcvgmul  15991  tsmsxp  24381  tgqioo  25026  ovolunlem2  25726  plyadd  26443  plymul  26444  coeeu  26451  nosupbnd1lem2  27945  noinfbnd1lem2  27960  tghilberti2  28985  cvmlift2lem10  35891  btwnconn1lem1  36667  btwnconn1lem2  36668  btwnconn1lem12  36678  lplnexllnN  40437  2llnjN  40440  4atlem12b  40484  lplncvrlvol2  40488  lncmp  40656  cdlema2N  40665  cdlemc2  41065  cdleme11a  41133  cdleme22eALTN  41218  cdleme24  41225  cdleme27a  41240  cdleme27N  41242  cdleme28  41246  cdlemefs29bpre0N  41289  cdlemefs29bpre1N  41290  cdlemefs29cpre1N  41291  cdlemefs29clN  41292  cdlemefs32fvaN  41295  cdlemefs32fva1  41296  cdleme36m  41334  cdleme39a  41338  cdleme17d3  41369  cdleme50trn2  41424  cdlemg36  41587  cdlemj3  41696  cdlemkfid1N  41794  cdlemkid1  41795  cdlemk19ylem  41803  cdlemk19xlem  41815  dihlsscpre  42107  dihord4  42131  dihatlat  42207  mapdh9a  42662  jm2.27  43849