Theorem truan 1518

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 1511	. . 3 ⊢ ⊤
2	1	biantrur 523	. 2 ⊢ (𝜑 ↔ (⊤ ∧ 𝜑))
3	2	bicomi 216	1 ⊢ ((⊤ ∧ 𝜑) ↔ 𝜑)

Syntax hints:   ↔ wb 198   ∧ wa 387  ⊤wtru 1508

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 199  df-an 388  df-tru 1510

This theorem is referenced by:  truanfal  1541  euelss  4171  tgcgr4  26013  aciunf1  30164  sgn3da  31445  truconj  34823  tradd  34827  ifpdfbi  39235  ifpdfxor  39249  dfid7  39335  eel0TT  40457  eelT00  40458  eelTTT  40459  eelT11  40460  eelT12  40462  eelTT1  40463  eelT01  40464  eel0T1  40465  eelTT  40524  uunT1p1  40534  uunTT1  40546  uunTT1p1  40547  uunTT1p2  40548  uunT11  40549  uunT11p1  40550  uunT11p2  40551  uunT12  40552  uunT12p1  40553  uunT12p2  40554  uunT12p3  40555  uunT12p4  40556  uunT12p5  40557