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  4278  sgn3da  15254  tgcgr4  28994  aciunf1  33257  wl-2mintru1  38413  truconj  39033  tradd  39037  ifpdfxor  44487  dfid7  44611  eel0TT  45685  eelT00  45686  eelTTT  45687  eelT11  45688  eelT12  45690  eelTT1  45691  eelT01  45692  eel0T1  45693  eelTT  45752  uunT1p1  45762  uunTT1  45774  uunTT1p1  45775  uunTT1p2  45776  uunT11  45777  uunT11p1  45778  uunT11p2  45779  uunT12  45780  uunT12p1  45781  uunT12p2  45782  uunT12p3  45783  uunT12p4  45784  uunT12p5  45785