Theorem truan 1552

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

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

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 1544

This theorem is referenced by:  truanfal  1575  euelss  4282  tgcgr4  28552  aciunf1  32690  sgn3da  32864  wl-2mintru1  37634  truconj  38241  tradd  38245  ifpdfxor  43670  dfid7  43795  eel0TT  44886  eelT00  44887  eelTTT  44888  eelT11  44889  eelT12  44891  eelTT1  44892  eelT01  44893  eel0T1  44894  eelTT  44953  uunT1p1  44963  uunTT1  44975  uunTT1p1  44976  uunTT1p2  44977  uunT11  44978  uunT11p1  44979  uunT11p2  44980  uunT12  44981  uunT12p1  44982  uunT12p2  44983  uunT12p3  44984  uunT12p4  44985  uunT12p5  44986