Theorem truan 1558

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 1551	. . 3 ⊢ ⊤
2	1	biantrur 535	. 2 ⊢ (𝜑 ↔ (⊤ ∧ 𝜑))
3	2	bicomi 225	1 ⊢ ((⊤ ∧ 𝜑) ↔ 𝜑)

Syntax hints:   ↔ wb 207   ∧ wa 396  ⊤wtru 1548

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 208  df-an 397  df-tru 1550

This theorem is referenced by:  truanfal  1581  euelss  4261  tgcgr4  28618  aciunf1  32756  sgn3da  32927  wl-2mintru1  37861  truconj  38477  tradd  38481  ifpdfxor  43940  dfid7  44065  eel0TT  45156  eelT00  45157  eelTTT  45158  eelT11  45159  eelT12  45161  eelTT1  45162  eelT01  45163  eel0T1  45164  eelTT  45223  uunT1p1  45233  uunTT1  45245  uunTT1p1  45246  uunTT1p2  45247  uunT11  45248  uunT11p1  45249  uunT11p2  45250  uunT12  45251  uunT12p1  45252  uunT12p2  45253  uunT12p3  45254  uunT12p4  45255  uunT12p5  45256