Theorem truan 1580

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

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

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 1572

This theorem is used by:  truanfal  1603  euelss  4277  sgn3da  15254  tgcgr4  28994  aciunf1  33257  wl-2mintru1  38414  truconj  39034  tradd  39038  ifpdfxor  44488  dfid7  44612  eel0TT  45686  eelT00  45687  eelTTT  45688  eelT11  45689  eelT12  45691  eelTT1  45692  eelT01  45693  eel0T1  45694  eelTT  45753  uunT1p1  45763  uunTT1  45775  uunTT1p1  45776  uunTT1p2  45777  uunT11  45778  uunT11p1  45779  uunT11p2  45780  uunT12  45781  uunT12p1  45782  uunT12p2  45783  uunT12p3  45784  uunT12p4  45785  uunT12p5  45786