Theorem truan 1387

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 1374	. . 3 |- T.
2	1	biantrur 506	. 2 |- ( ph <-> ( T. /\ ph ) )
3	2	bicomi 202	1 |- ( ( T. /\ ph ) <-> ph )

Syntax hints:   <-> wb 184   /\ wa 369   T. wtru 1371

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 185  df-an 371  df-tru 1373

This theorem is referenced by:  truanfal  1395  sgn3da  27060  truconj  29044  tradd  29050  eel0TT  31730  eelT00  31731  eelTTT  31732  eelT11  31734  eelT12  31738  eelTT1  31740  eelT01  31741  eel0T1  31742  eelTT  31806  uunT1p1  31816  uunTT1  31828  uunTT1p1  31829  uunTT1p2  31830  uunT11  31831  uunT11p1  31832  uunT11p2  31833  uunT12  31834  uunT12p1  31835  uunT12p2  31836  uunT12p3  31837  uunT12p4  31838  uunT12p5  31839