Theorem truan 1492

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 1479	. . 3 ⊢ ⊤
2	1	biantrur 526	. 2 ⊢ (𝜑 ↔ (⊤ ∧ 𝜑))
3	2	bicomi 213	1 ⊢ ((⊤ ∧ 𝜑) ↔ 𝜑)

Syntax hints:   ↔ wb 195   ∧ wa 383  ⊤wtru 1476

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 196  df-an 385  df-tru 1478

This theorem is referenced by:  truanfal  1498  euelss  3873  tgcgr4  25226  aciunf1  28845  sgn3da  29930  truconj  33073  tradd  33077  ifpdfbi  36837  ifpdfxor  36851  dfid7  36938  eel0TT  37950  eelT00  37951  eelTTT  37952  eelT11  37953  eelT12  37955  eelTT1  37956  eelT01  37957  eel0T1  37958  eelTT  38019  uunT1p1  38029  uunTT1  38041  uunTT1p1  38042  uunTT1p2  38043  uunT11  38044  uunT11p1  38045  uunT11p2  38046  uunT12  38047  uunT12p1  38048  uunT12p2  38049  uunT12p3  38050  uunT12p4  38051  uunT12p5  38052