Theorem truan 1552

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

Syntax hints:   ↔ wb 205   ∧ wa 396  ⊤wtru 1542

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 397  df-tru 1544

This theorem is referenced by:  truanfal  1575  euelss  4286  tgcgr4  27536  aciunf1  31646  sgn3da  33230  wl-2mintru1  36034  truconj  36633  tradd  36637  ifpdfxor  41881  dfid7  42006  eel0TT  43108  eelT00  43109  eelTTT  43110  eelT11  43111  eelT12  43113  eelTT1  43114  eelT01  43115  eel0T1  43116  eelTT  43175  uunT1p1  43185  uunTT1  43197  uunTT1p1  43198  uunTT1p2  43199  uunT11  43200  uunT11p1  43201  uunT11p2  43202  uunT12  43203  uunT12p1  43204  uunT12p2  43205  uunT12p3  43206  uunT12p4  43207  uunT12p5  43208