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

Syntax hints:   ↔ wb 205   ∧ wa 395  ⊤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 396  df-tru 1544

This theorem is referenced by:  truanfal  1575  euelss  4260  tgcgr4  26873  aciunf1  30979  sgn3da  32487  wl-2mintru1  35640  truconj  36238  tradd  36242  ifpdfxor  41056  dfid7  41173  eel0TT  42277  eelT00  42278  eelTTT  42279  eelT11  42280  eelT12  42282  eelTT1  42283  eelT01  42284  eel0T1  42285  eelTT  42344  uunT1p1  42354  uunTT1  42366  uunTT1p1  42367  uunTT1p2  42368  uunT11  42369  uunT11p1  42370  uunT11p2  42371  uunT12  42372  uunT12p1  42373  uunT12p2  42374  uunT12p3  42375  uunT12p4  42376  uunT12p5  42377