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

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

This theorem is referenced by:  truanfal  1573  euelss  4255  tgcgr4  26892  aciunf1  31000  sgn3da  32508  wl-2mintru1  35661  truconj  36259  tradd  36263  ifpdfxor  41094  dfid7  41220  eel0TT  42324  eelT00  42325  eelTTT  42326  eelT11  42327  eelT12  42329  eelTT1  42330  eelT01  42331  eel0T1  42332  eelTT  42391  uunT1p1  42401  uunTT1  42413  uunTT1p1  42414  uunTT1p2  42415  uunT11  42416  uunT11p1  42417  uunT11p2  42418  uunT12  42419  uunT12p1  42420  uunT12p2  42421  uunT12p3  42422  uunT12p4  42423  uunT12p5  42424