Theorem truan 1416

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

Syntax hints:   <-> wb 184   /\ wa 367   T. wtru 1400

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 369  df-tru 1402

This theorem is referenced by:  truanfal  1424  euelss  3727  aciunf1  27683  sgn3da  28703  truconj  30707  tradd  30713  eel0TT  33871  eelT00  33872  eelTTT  33873  eelT11  33875  eelT12  33879  eelTT1  33881  eelT01  33882  eel0T1  33883  eelTT  33947  uunT1p1  33957  uunTT1  33969  uunTT1p1  33970  uunTT1p2  33971  uunT11  33972  uunT11p1  33973  uunT11p2  33974  uunT12  33975  uunT12p1  33976  uunT12p2  33977  uunT12p3  33978  uunT12p4  33979  uunT12p5  33980  ifpdfbi  38195  ifpdfxor  38201