Theorem truan 1581

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

This proof depends on syntax axioms:   ↔ wb 209   ∧ wa 401  ⊤wtru 1571

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573

This theorem is used by:  truanfal  1604  euelss  4285  sgn3da  15166  tgcgr4  28855  aciunf1  33083  wl-2mintru1  38197  truconj  38812  tradd  38816  ifpdfxor  44290  dfid7  44415  eel0TT  45489  eelT00  45490  eelTTT  45491  eelT11  45492  eelT12  45494  eelTT1  45495  eelT01  45496  eel0T1  45497  eelTT  45556  uunT1p1  45566  uunTT1  45578  uunTT1p1  45579  uunTT1p2  45580  uunT11  45581  uunT11p1  45582  uunT11p2  45583  uunT12  45584  uunT12p1  45585  uunT12p2  45586  uunT12p3  45587  uunT12p4  45588  uunT12p5  45589