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  4280  sgn3da  15269  tgcgr4  29009  aciunf1  33314  wl-2mintru1  38559  truconj  39179  tradd  39183  ifpdfxor  44634  dfid7  44758  eel0TT  45831  eelT00  45832  eelTTT  45833  eelT11  45834  eelT12  45836  eelTT1  45837  eelT01  45838  eel0T1  45839  eelTT  45898  uunT1p1  45908  uunTT1  45920  uunTT1p1  45921  uunTT1p2  45922  uunT11  45923  uunT11p1  45924  uunT11p2  45925  uunT12  45926  uunT12p1  45927  uunT12p2  45928  uunT12p3  45929  uunT12p4  45930  uunT12p5  45931