Theorem truan 1551

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

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

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 1543

This theorem is referenced by:  truanfal  1574  euelss  4283  tgcgr4  28476  aciunf1  32607  sgn3da  32780  wl-2mintru1  37474  truconj  38091  tradd  38095  ifpdfxor  43470  dfid7  43595  eel0TT  44687  eelT00  44688  eelTTT  44689  eelT11  44690  eelT12  44692  eelTT1  44693  eelT01  44694  eel0T1  44695  eelTT  44754  uunT1p1  44764  uunTT1  44776  uunTT1p1  44777  uunTT1p2  44778  uunT11  44779  uunT11p1  44780  uunT11p2  44781  uunT12  44782  uunT12p1  44783  uunT12p2  44784  uunT12p3  44785  uunT12p4  44786  uunT12p5  44787