Theorem truan 1572

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 1565	. . 3 ⊢ ⊤
2	1	biantrur 538	. 2 ⊢ (𝜑 ↔ (⊤ ∧ 𝜑))
3	2	bicomi 226	1 ⊢ ((⊤ ∧ 𝜑) ↔ 𝜑)

Syntax hints:   ↔ wb 208   ∧ wa 399  ⊤wtru 1562

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-tru 1564

This theorem is referenced by:  truanfal  1595  euelss  4285  sgn3da  15115  tgcgr4  28701  aciunf1  32866  wl-2mintru1  37985  truconj  38601  tradd  38605  ifpdfxor  44064  dfid7  44189  eel0TT  45280  eelT00  45281  eelTTT  45282  eelT11  45283  eelT12  45285  eelTT1  45286  eelT01  45287  eel0T1  45288  eelTT  45347  uunT1p1  45357  uunTT1  45369  uunTT1p1  45370  uunTT1p2  45371  uunT11  45372  uunT11p1  45373  uunT11p2  45374  uunT12  45375  uunT12p1  45376  uunT12p2  45377  uunT12p3  45378  uunT12p4  45379  uunT12p5  45380