Theorem truan 1549

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 1542	. . 3 ⊢ ⊤
2	1	biantrur 534	. 2 ⊢ (𝜑 ↔ (⊤ ∧ 𝜑))
3	2	bicomi 227	1 ⊢ ((⊤ ∧ 𝜑) ↔ 𝜑)

Syntax hints:   ↔ wb 209   ∧ wa 399  ⊤wtru 1539

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 210  df-an 400  df-tru 1541

This theorem is referenced by:  truanfal  1572  euelss  4242  tgcgr4  26325  aciunf1  30426  sgn3da  31909  wl-2mintru1  34907  truconj  35539  tradd  35543  ifpdfxor  40195  dfid7  40312  eel0TT  41410  eelT00  41411  eelTTT  41412  eelT11  41413  eelT12  41415  eelTT1  41416  eelT01  41417  eel0T1  41418  eelTT  41477  uunT1p1  41487  uunTT1  41499  uunTT1p1  41500  uunTT1p2  41501  uunT11  41502  uunT11p1  41503  uunT11p2  41504  uunT12  41505  uunT12p1  41506  uunT12p2  41507  uunT12p3  41508  uunT12p4  41509  uunT12p5  41510