Theorem truan 1544

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

Syntax hints:   ↔ wb 205   ∧ wa 394  ⊤wtru 1534

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 395  df-tru 1536

This theorem is referenced by:  truanfal  1567  euelss  4322  tgcgr4  28391  aciunf1  32506  sgn3da  34231  wl-2mintru1  37039  truconj  37644  tradd  37648  ifpdfxor  42982  dfid7  43107  eel0TT  44208  eelT00  44209  eelTTT  44210  eelT11  44211  eelT12  44213  eelTT1  44214  eelT01  44215  eel0T1  44216  eelTT  44275  uunT1p1  44285  uunTT1  44297  uunTT1p1  44298  uunTT1p2  44299  uunT11  44300  uunT11p1  44301  uunT11p2  44302  uunT12  44303  uunT12p1  44304  uunT12p2  44305  uunT12p3  44306  uunT12p4  44307  uunT12p5  44308