Theorem truan 1551

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

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

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 1543

This theorem is referenced by:  truanfal  1574  euelss  4312  tgcgr4  28515  aciunf1  32646  sgn3da  32818  wl-2mintru1  37513  truconj  38130  tradd  38134  ifpdfxor  43478  dfid7  43603  eel0TT  44695  eelT00  44696  eelTTT  44697  eelT11  44698  eelT12  44700  eelTT1  44701  eelT01  44702  eel0T1  44703  eelTT  44762  uunT1p1  44772  uunTT1  44784  uunTT1p1  44785  uunTT1p2  44786  uunT11  44787  uunT11p1  44788  uunT11p2  44789  uunT12  44790  uunT12p1  44791  uunT12p2  44792  uunT12p3  44793  uunT12p4  44794  uunT12p5  44795