Theorem truan 1553

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 1546	. . 3 ⊢ ⊤
2	1	biantrur 530	. 2 ⊢ (𝜑 ↔ (⊤ ∧ 𝜑))
3	2	bicomi 224	1 ⊢ ((⊤ ∧ 𝜑) ↔ 𝜑)

Syntax hints:   ↔ wb 206   ∧ wa 395  ⊤wtru 1543

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545

This theorem is referenced by:  truanfal  1576  euelss  4273  tgcgr4  28613  aciunf1  32751  sgn3da  32922  wl-2mintru1  37820  truconj  38436  tradd  38440  ifpdfxor  43932  dfid7  44057  eel0TT  45148  eelT00  45149  eelTTT  45150  eelT11  45151  eelT12  45153  eelTT1  45154  eelT01  45155  eel0T1  45156  eelTT  45215  uunT1p1  45225  uunTT1  45237  uunTT1p1  45238  uunTT1p2  45239  uunT11  45240  uunT11p1  45241  uunT11p2  45242  uunT12  45243  uunT12p1  45244  uunT12p2  45245  uunT12p3  45246  uunT12p4  45247  uunT12p5  45248