![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
Mirrors > Home > MPE Home > Th. List > truan | Structured version Unicode version |
Description: True can be removed from a conjunction. (Contributed by FL, 20-Mar-2011.) (Proof shortened by Wolf Lammen, 21-Jul-2019.) |
Ref | Expression |
---|---|
truan |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | tru 1374 |
. . 3
![]() ![]() | |
2 | 1 | biantrur 506 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
3 | 2 | bicomi 202 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff setvar class |
Syntax hints: ![]() ![]() ![]() |
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 |
Copyright terms: Public domain | W3C validator |