Theorem truan 1454

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 1441	. . 3 |- T.
2	1	biantrur 508	. 2 |- ( ph <-> ( T. /\ ph ) )
3	2	bicomi 205	1 |- ( ( T. /\ ph ) <-> ph )

Syntax hints:   <-> wb 187   /\ wa 370   T. wtru 1438

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 188  df-an 372  df-tru 1440

This theorem is referenced by:  truanfal  1460  euelss  3760  tgcgr4  24574  aciunf1  28267  sgn3da  29420  truconj  32301  tradd  32306  ifpdfbi  36087  ifpdfxor  36101  dfid7  36189  eel0TT  37056  eelT00  37057  eelTTT  37058  eelT11  37060  eelT12  37064  eelTT1  37066  eelT01  37067  eel0T1  37068  eelTT  37131  uunT1p1  37141  uunTT1  37153  uunTT1p1  37154  uunTT1p2  37155  uunT11  37156  uunT11p1  37157  uunT11p2  37158  uunT12  37159  uunT12p1  37160  uunT12p2  37161  uunT12p3  37162  uunT12p4  37163  uunT12p5  37164