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  15177  tgcgr4  28876  aciunf1  33139  wl-2mintru1  38247  truconj  38852  tradd  38856  ifpdfxor  44330  dfid7  44455  eel0TT  45529  eelT00  45530  eelTTT  45531  eelT11  45532  eelT12  45534  eelTT1  45535  eelT01  45536  eel0T1  45537  eelTT  45596  uunT1p1  45606  uunTT1  45618  uunTT1p1  45619  uunTT1p2  45620  uunT11  45621  uunT11p1  45622  uunT11p2  45623  uunT12  45624  uunT12p1  45625  uunT12p2  45626  uunT12p3  45627  uunT12p4  45628  uunT12p5  45629