Theorem truan 1548

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

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

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 1540

This theorem is referenced by:  truanfal  1571  euelss  4338  tgcgr4  28554  aciunf1  32680  sgn3da  34523  wl-2mintru1  37473  truconj  38088  tradd  38092  ifpdfxor  43477  dfid7  43602  eel0TT  44702  eelT00  44703  eelTTT  44704  eelT11  44705  eelT12  44707  eelTT1  44708  eelT01  44709  eel0T1  44710  eelTT  44769  uunT1p1  44779  uunTT1  44791  uunTT1p1  44792  uunTT1p2  44793  uunT11  44794  uunT11p1  44795  uunT11p2  44796  uunT12  44797  uunT12p1  44798  uunT12p2  44799  uunT12p3  44800  uunT12p4  44801  uunT12p5  44802