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  4286  tgcgr4  28619  aciunf1  32757  sgn3da  32930  wl-2mintru1  37749  truconj  38356  tradd  38360  ifpdfxor  43847  dfid7  43972  eel0TT  45063  eelT00  45064  eelTTT  45065  eelT11  45066  eelT12  45068  eelTT1  45069  eelT01  45070  eel0T1  45071  eelTT  45130  uunT1p1  45140  uunTT1  45152  uunTT1p1  45153  uunTT1p2  45154  uunT11  45155  uunT11p1  45156  uunT11p2  45157  uunT12  45158  uunT12p1  45159  uunT12p2  45160  uunT12p3  45161  uunT12p4  45162  uunT12p5  45163