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  8508  hashbclem  14363  ntrivcvgmul  15813  tsmsxp  24073  tgqioo  24718  ovolunlem2  25429  plyadd  26152  plymul  26153  coeeu  26160  nosupbnd1lem2  27651  noinfbnd1lem2  27666  tghilberti2  28619  cvmlift2lem10  35379  btwnconn1lem1  36154  btwnconn1lem2  36155  btwnconn1lem12  36165  lplnexllnN  39686  2llnjN  39689  4atlem12b  39733  lplncvrlvol2  39737  lncmp  39905  cdlema2N  39914  cdlemc2  40314  cdleme11a  40382  cdleme22eALTN  40467  cdleme24  40474  cdleme27a  40489  cdleme27N  40491  cdleme28  40495  cdlemefs29bpre0N  40538  cdlemefs29bpre1N  40539  cdlemefs29cpre1N  40540  cdlemefs29clN  40541  cdlemefs32fvaN  40544  cdlemefs32fva1  40545  cdleme36m  40583  cdleme39a  40587  cdleme17d3  40618  cdleme50trn2  40673  cdlemg36  40836  cdlemj3  40945  cdlemkfid1N  41043  cdlemkid1  41044  cdlemk19ylem  41052  cdlemk19xlem  41064  dihlsscpre  41356  dihord4  41380  dihatlat  41456  mapdh9a  41911  jm2.27  43128