Theorem truan 1553

Description: True can be removed from a conjunction. (Contributed by FL, 20-Mar-2011.) (Proof shortened by Wolf Lammen, 21-Jul-2019.)

Assertion

Ref	Expression
truan	⊢ ((⊤ ∧ 𝜑) ↔ 𝜑)

Proof of Theorem truan

Step	Hyp	Ref	Expression
1		tru 1546	. . 3 ⊢ ⊤
2	1	biantrur 532	. 2 ⊢ (𝜑 ↔ (⊤ ∧ 𝜑))
3	2	bicomi 223	1 ⊢ ((⊤ ∧ 𝜑) ↔ 𝜑)

Syntax hints:   ↔ wb 205   ∧ wa 397  ⊤wtru 1543

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 398  df-tru 1545

This theorem is referenced by:  truanfal  1576  euelss  4322  tgcgr4  27782  aciunf1  31888  sgn3da  33540  wl-2mintru1  36371  truconj  36969  tradd  36973  ifpdfxor  42238  dfid7  42363  eel0TT  43465  eelT00  43466  eelTTT  43467  eelT11  43468  eelT12  43470  eelTT1  43471  eelT01  43472  eel0T1  43473  eelTT  43532  uunT1p1  43542  uunTT1  43554  uunTT1p1  43555  uunTT1p2  43556  uunT11  43557  uunT11p1  43558  uunT11p2  43559  uunT12  43560  uunT12p1  43561  uunT12p2  43562  uunT12p3  43563  uunT12p4  43564  uunT12p5  43565