Theorem simp3rl 1259

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

Assertion

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

Proof of Theorem simp3rl

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

Syntax hints:   → wi 4   ∧ wa 399   ∧ w3a 1097

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 209  df-an 400  df-3an 1099

This theorem is referenced by:  omeu  8547  hashbclem  14458  ntrivcvgmul  15922  tsmsxp  24202  tgqioo  24847  ovolunlem2  25547  plyadd  26264  plymul  26265  coeeu  26272  nosupbnd1lem2  27760  noinfbnd1lem2  27775  tghilberti2  28794  cvmlift2lem10  35622  btwnconn1lem1  36397  btwnconn1lem2  36398  btwnconn1lem12  36408  lplnexllnN  40148  2llnjN  40151  4atlem12b  40195  lplncvrlvol2  40199  lncmp  40367  cdlema2N  40376  cdlemc2  40776  cdleme11a  40844  cdleme22eALTN  40929  cdleme24  40936  cdleme27a  40951  cdleme27N  40953  cdleme28  40957  cdlemefs29bpre0N  41000  cdlemefs29bpre1N  41001  cdlemefs29cpre1N  41002  cdlemefs29clN  41003  cdlemefs32fvaN  41006  cdlemefs32fva1  41007  cdleme36m  41045  cdleme39a  41049  cdleme17d3  41080  cdleme50trn2  41135  cdlemg36  41298  cdlemj3  41407  cdlemkfid1N  41505  cdlemkid1  41506  cdlemk19ylem  41514  cdlemk19xlem  41526  dihlsscpre  41818  dihord4  41842  dihatlat  41918  mapdh9a  42373  jm2.27  43545