Theorem simp3rl 1247

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

Assertion

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

Proof of Theorem simp3rl

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

Syntax hints:   → wi 4   ∧ wa 395   ∧ 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 207  df-an 396  df-3an 1088

This theorem is referenced by:  omeu  8597  hashbclem  14470  ntrivcvgmul  15918  tsmsxp  24093  tgqioo  24739  ovolunlem2  25451  plyadd  26174  plymul  26175  coeeu  26182  nosupbnd1lem2  27673  noinfbnd1lem2  27688  tghilberti2  28617  cvmlift2lem10  35334  btwnconn1lem1  36105  btwnconn1lem2  36106  btwnconn1lem12  36116  lplnexllnN  39583  2llnjN  39586  4atlem12b  39630  lplncvrlvol2  39634  lncmp  39802  cdlema2N  39811  cdlemc2  40211  cdleme11a  40279  cdleme22eALTN  40364  cdleme24  40371  cdleme27a  40386  cdleme27N  40388  cdleme28  40392  cdlemefs29bpre0N  40435  cdlemefs29bpre1N  40436  cdlemefs29cpre1N  40437  cdlemefs29clN  40438  cdlemefs32fvaN  40441  cdlemefs32fva1  40442  cdleme36m  40480  cdleme39a  40484  cdleme17d3  40515  cdleme50trn2  40570  cdlemg36  40733  cdlemj3  40842  cdlemkfid1N  40940  cdlemkid1  40941  cdlemk19ylem  40949  cdlemk19xlem  40961  dihlsscpre  41253  dihord4  41277  dihatlat  41353  mapdh9a  41808  jm2.27  43032