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  4297  tgcgr4  28464  aciunf1  32593  sgn3da  32765  wl-2mintru1  37473  truconj  38090  tradd  38094  ifpdfxor  43469  dfid7  43594  eel0TT  44686  eelT00  44687  eelTTT  44688  eelT11  44689  eelT12  44691  eelTT1  44692  eelT01  44693  eel0T1  44694  eelTT  44753  uunT1p1  44763  uunTT1  44775  uunTT1p1  44776  uunTT1p2  44777  uunT11  44778  uunT11p1  44779  uunT11p2  44780  uunT12  44781  uunT12p1  44782  uunT12p2  44783  uunT12p3  44784  uunT12p4  44785  uunT12p5  44786