Theorem simp3rl 1245

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

Assertion

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

Proof of Theorem simp3rl

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

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

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 206  df-an 397  df-3an 1088

This theorem is referenced by:  omeu  8416  hashbclem  14164  ntrivcvgmul  15614  tsmsxp  23306  tgqioo  23963  ovolunlem2  24662  plyadd  25378  plymul  25379  coeeu  25386  tghilberti2  26999  cvmlift2lem10  33274  nosupbnd1lem2  33912  noinfbnd1lem2  33927  btwnconn1lem1  34389  btwnconn1lem2  34390  btwnconn1lem12  34400  lplnexllnN  37578  2llnjN  37581  4atlem12b  37625  lplncvrlvol2  37629  lncmp  37797  cdlema2N  37806  cdlemc2  38206  cdleme11a  38274  cdleme22eALTN  38359  cdleme24  38366  cdleme27a  38381  cdleme27N  38383  cdleme28  38387  cdlemefs29bpre0N  38430  cdlemefs29bpre1N  38431  cdlemefs29cpre1N  38432  cdlemefs29clN  38433  cdlemefs32fvaN  38436  cdlemefs32fva1  38437  cdleme36m  38475  cdleme39a  38479  cdleme17d3  38510  cdleme50trn2  38565  cdlemg36  38728  cdlemj3  38837  cdlemkfid1N  38935  cdlemkid1  38936  cdlemk19ylem  38944  cdlemk19xlem  38956  dihlsscpre  39248  dihord4  39272  dihatlat  39348  mapdh9a  39803  jm2.27  40830