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  4273  tgcgr4  28617  aciunf1  32755  sgn3da  32926  wl-2mintru1  37824  truconj  38440  tradd  38444  ifpdfxor  43936  dfid7  44061  eel0TT  45152  eelT00  45153  eelTTT  45154  eelT11  45155  eelT12  45157  eelTT1  45158  eelT01  45159  eel0T1  45160  eelTT  45219  uunT1p1  45229  uunTT1  45241  uunTT1p1  45242  uunTT1p2  45243  uunT11  45244  uunT11p1  45245  uunT11p2  45246  uunT12  45247  uunT12p1  45248  uunT12p2  45249  uunT12p3  45250  uunT12p4  45251  uunT12p5  45252