Theorem truan 1545

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 1538	. . 3 ⊢ ⊤
2	1	biantrur 530	. 2 ⊢ (𝜑 ↔ (⊤ ∧ 𝜑))
3	2	bicomi 223	1 ⊢ ((⊤ ∧ 𝜑) ↔ 𝜑)

Syntax hints:   ↔ wb 205   ∧ wa 395  ⊤wtru 1535

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 396  df-tru 1537

This theorem is referenced by:  truanfal  1568  euelss  4317  tgcgr4  28322  aciunf1  32432  sgn3da  34097  wl-2mintru1  36905  truconj  37509  tradd  37513  ifpdfxor  42840  dfid7  42965  eel0TT  44066  eelT00  44067  eelTTT  44068  eelT11  44069  eelT12  44071  eelTT1  44072  eelT01  44073  eel0T1  44074  eelTT  44133  uunT1p1  44143  uunTT1  44155  uunTT1p1  44156  uunTT1p2  44157  uunT11  44158  uunT11p1  44159  uunT11p2  44160  uunT12  44161  uunT12p1  44162  uunT12p2  44163  uunT12p3  44164  uunT12p4  44165  uunT12p5  44166