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  4307  tgcgr4  28456  aciunf1  32587  sgn3da  32759  wl-2mintru1  37454  truconj  38071  tradd  38075  ifpdfxor  43458  dfid7  43583  eel0TT  44676  eelT00  44677  eelTTT  44678  eelT11  44679  eelT12  44681  eelTT1  44682  eelT01  44683  eel0T1  44684  eelTT  44743  uunT1p1  44753  uunTT1  44765  uunTT1p1  44766  uunTT1p2  44767  uunT11  44768  uunT11p1  44769  uunT11p2  44770  uunT12  44771  uunT12p1  44772  uunT12p2  44773  uunT12p3  44774  uunT12p4  44775  uunT12p5  44776