Theorem truan 1578

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 1571	. . 3 ⊢ ⊤
2	1	biantrur 539	. 2 ⊢ (𝜑 ↔ (⊤ ∧ 𝜑))
3	2	bicomi 227	1 ⊢ ((⊤ ∧ 𝜑) ↔ 𝜑)

Syntax hints:   ↔ wb 209   ∧ wa 400  ⊤wtru 1568

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 210  df-an 401  df-tru 1570

This theorem is referenced by:  truanfal  1601  euelss  4293  sgn3da  15138  tgcgr4  28766  aciunf1  32949  wl-2mintru1  38058  truconj  38674  tradd  38678  ifpdfxor  44139  dfid7  44264  eel0TT  45338  eelT00  45339  eelTTT  45340  eelT11  45341  eelT12  45343  eelTT1  45344  eelT01  45345  eel0T1  45346  eelTT  45405  uunT1p1  45415  uunTT1  45427  uunTT1p1  45428  uunTT1p2  45429  uunT11  45430  uunT11p1  45431  uunT11p2  45432  uunT12  45433  uunT12p1  45434  uunT12p2  45435  uunT12p3  45436  uunT12p4  45437  uunT12p5  45438