Theorem truan 1550

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

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

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 1542

This theorem is referenced by:  truanfal  1573  euelss  4331  tgcgr4  28540  aciunf1  32674  sgn3da  34545  wl-2mintru1  37492  truconj  38109  tradd  38113  ifpdfxor  43505  dfid7  43630  eel0TT  44729  eelT00  44730  eelTTT  44731  eelT11  44732  eelT12  44734  eelTT1  44735  eelT01  44736  eel0T1  44737  eelTT  44796  uunT1p1  44806  uunTT1  44818  uunTT1p1  44819  uunTT1p2  44820  uunT11  44821  uunT11p1  44822  uunT11p2  44823  uunT12  44824  uunT12p1  44825  uunT12p2  44826  uunT12p3  44827  uunT12p4  44828  uunT12p5  44829