Theorem truan 1501

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	|- ( ( T. /\ ph ) <-> ph )

Proof of Theorem truan

Step	Hyp	Ref	Expression
1		tru 1487	. . 3 |- T.
2	1	biantrur 527	. 2 |- ( ph <-> ( T. /\ ph ) )
3	2	bicomi 214	1 |- ( ( T. /\ ph ) <-> ph )

Syntax hints:   <-> wb 196   /\ wa 384   T. wtru 1484

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 197  df-an 386  df-tru 1486

This theorem is referenced by:  truanfal  1507  euelss  3914  tgcgr4  25426  aciunf1  29463  sgn3da  30603  truconj  33903  tradd  33907  ifpdfbi  37818  ifpdfxor  37832  dfid7  37919  eel0TT  38929  eelT00  38930  eelTTT  38931  eelT11  38932  eelT12  38934  eelTT1  38935  eelT01  38936  eel0T1  38937  eelTT  38998  uunT1p1  39008  uunTT1  39020  uunTT1p1  39021  uunTT1p2  39022  uunT11  39023  uunT11p1  39024  uunT11p2  39025  uunT12  39026  uunT12p1  39027  uunT12p2  39028  uunT12p3  39029  uunT12p4  39030  uunT12p5  39031