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 224	1 ⊢ ((⊤ ∧ 𝜑) ↔ 𝜑)

Syntax hints:   ↔ wb 206   ∧ 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 207  df-an 396  df-tru 1544

This theorem is referenced by:  truanfal  1575  euelss  4284  tgcgr4  28605  aciunf1  32743  sgn3da  32917  wl-2mintru1  37697  truconj  38304  tradd  38308  ifpdfxor  43749  dfid7  43874  eel0TT  44965  eelT00  44966  eelTTT  44967  eelT11  44968  eelT12  44970  eelTT1  44971  eelT01  44972  eel0T1  44973  eelTT  45032  uunT1p1  45042  uunTT1  45054  uunTT1p1  45055  uunTT1p2  45056  uunT11  45057  uunT11p1  45058  uunT11p2  45059  uunT12  45060  uunT12p1  45061  uunT12p2  45062  uunT12p3  45063  uunT12p4  45064  uunT12p5  45065