Theorem truan 1614

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 1600	. . 3 ⊢ ⊤
2	1	biantrur 528	. 2 ⊢ (𝜑 ↔ (⊤ ∧ 𝜑))
3	2	bicomi 214	1 ⊢ ((⊤ ∧ 𝜑) ↔ 𝜑)

Syntax hints:   ↔ wb 196   ∧ wa 383  ⊤wtru 1597

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 197  df-an 385  df-tru 1599

This theorem is referenced by:  truanfal  1620  euelss  4022  tgcgr4  25546  aciunf1  29693  sgn3da  30833  truconj  34135  tradd  34139  ifpdfbi  38237  ifpdfxor  38251  dfid7  38338  eel0TT  39348  eelT00  39349  eelTTT  39350  eelT11  39351  eelT12  39353  eelTT1  39354  eelT01  39355  eel0T1  39356  eelTT  39417  uunT1p1  39427  uunTT1  39439  uunTT1p1  39440  uunTT1p2  39441  uunT11  39442  uunT11p1  39443  uunT11p2  39444  uunT12  39445  uunT12p1  39446  uunT12p2  39447  uunT12p3  39448  uunT12p4  39449  uunT12p5  39450