Theorem truan 1550

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

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

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 1542

This theorem is referenced by:  truanfal  1573  euelss  4252  tgcgr4  26796  aciunf1  30902  sgn3da  32408  wl-2mintru1  35588  truconj  36186  tradd  36190  ifpdfxor  40992  dfid7  41109  eel0TT  42213  eelT00  42214  eelTTT  42215  eelT11  42216  eelT12  42218  eelTT1  42219  eelT01  42220  eel0T1  42221  eelTT  42280  uunT1p1  42290  uunTT1  42302  uunTT1p1  42303  uunTT1p2  42304  uunT11  42305  uunT11p1  42306  uunT11p2  42307  uunT12  42308  uunT12p1  42309  uunT12p2  42310  uunT12p3  42311  uunT12p4  42312  uunT12p5  42313