Theorem truan 1553

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

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

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 1545

This theorem is referenced by:  truanfal  1576  euelss  4272  tgcgr4  28599  aciunf1  32736  sgn3da  32907  wl-2mintru1  37806  truconj  38422  tradd  38426  ifpdfxor  43914  dfid7  44039  eel0TT  45130  eelT00  45131  eelTTT  45132  eelT11  45133  eelT12  45135  eelTT1  45136  eelT01  45137  eel0T1  45138  eelTT  45197  uunT1p1  45207  uunTT1  45219  uunTT1p1  45220  uunTT1p2  45221  uunT11  45222  uunT11p1  45223  uunT11p2  45224  uunT12  45225  uunT12p1  45226  uunT12p2  45227  uunT12p3  45228  uunT12p4  45229  uunT12p5  45230