Theorem truan 1548

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 1541	. . 3 ⊢ ⊤
2	1	biantrur 533	. 2 ⊢ (𝜑 ↔ (⊤ ∧ 𝜑))
3	2	bicomi 226	1 ⊢ ((⊤ ∧ 𝜑) ↔ 𝜑)

Syntax hints:   ↔ wb 208   ∧ wa 398  ⊤wtru 1538

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 209  df-an 399  df-tru 1540

This theorem is referenced by:  truanfal  1571  euelss  4292  tgcgr4  26319  aciunf1  30410  sgn3da  31801  truconj  35381  tradd  35385  ifpdfbi  39846  ifpdfxor  39860  dfid7  39979  eel0TT  41045  eelT00  41046  eelTTT  41047  eelT11  41048  eelT12  41050  eelTT1  41051  eelT01  41052  eel0T1  41053  eelTT  41112  uunT1p1  41122  uunTT1  41134  uunTT1p1  41135  uunTT1p2  41136  uunT11  41137  uunT11p1  41138  uunT11p2  41139  uunT12  41140  uunT12p1  41141  uunT12p2  41142  uunT12p3  41143  uunT12p4  41144  uunT12p5  41145