Theorem truan 1552

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

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

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 1544

This theorem is referenced by:  truanfal  1575  euelss  4279  tgcgr4  28509  aciunf1  32645  sgn3da  32817  wl-2mintru1  37534  truconj  38151  tradd  38155  ifpdfxor  43590  dfid7  43715  eel0TT  44806  eelT00  44807  eelTTT  44808  eelT11  44809  eelT12  44811  eelTT1  44812  eelT01  44813  eel0T1  44814  eelTT  44873  uunT1p1  44883  uunTT1  44895  uunTT1p1  44896  uunTT1p2  44897  uunT11  44898  uunT11p1  44899  uunT11p2  44900  uunT12  44901  uunT12p1  44902  uunT12p2  44903  uunT12p3  44904  uunT12p4  44905  uunT12p5  44906