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

This proof depends on syntax axioms:   ↔ wb 209   ∧ wa 400  ⊤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 401  df-tru 1573

This theorem is used by:  truanfal  1604  euelss  4285  sgn3da  15143  tgcgr4  28809  aciunf1  33017  wl-2mintru1  38164  truconj  38778  tradd  38782  ifpdfxor  44241  dfid7  44366  eel0TT  45440  eelT00  45441  eelTTT  45442  eelT11  45443  eelT12  45445  eelTT1  45446  eelT01  45447  eel0T1  45448  eelTT  45507  uunT1p1  45517  uunTT1  45529  uunTT1p1  45530  uunTT1p2  45531  uunT11  45532  uunT11p1  45533  uunT11p2  45534  uunT12  45535  uunT12p1  45536  uunT12p2  45537  uunT12p3  45538  uunT12p4  45539  uunT12p5  45540