![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > biadan2 | Structured version Visualization version Unicode version |
Description: Add a conjunction to an equivalence. (Contributed by Jeff Madsen, 20-Jun-2011.) |
Ref | Expression |
---|---|
biadan2.1 |
![]() ![]() ![]() ![]() ![]() ![]() |
biadan2.2 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
biadan2 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | biadan2.1 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() | |
2 | 1 | pm4.71ri 639 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
3 | biadan2.2 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
4 | 3 | pm5.32i 643 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
5 | 2, 4 | bitri 253 |
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 189 df-an 373 |
This theorem is referenced by: elab4g 3191 brab2a 4887 brab2ga 4913 elovmpt2 6519 eqop2 6839 iscard 8414 iscard2 8415 elnnnn0 10920 elfzo2 11930 bitsval 14409 1nprm 14641 funcpropd 15817 isfull 15827 isfth 15831 ismhm 16596 isghm 16895 ghmpropd 16932 isga 16957 oppgcntz 17027 gexdvdsi 17246 isrhm 17961 abvpropd 18082 islmhm 18262 dfprm2 19077 prmirred 19078 elocv 19243 isobs 19295 iscn2 20266 iscnp2 20267 islocfin 20544 elflim2 20991 isfcls 21036 isnghm 21740 isnghmOLD 21758 isnmhm 21779 0plef 22642 elply 23161 dchrelbas4 24183 nb3grapr 25193 isph 26475 abfmpunirn 28263 iscvm 29994 sscoid 30692 eldiophb 35611 eldioph3b 35619 eldioph4b 35666 issdrg 36075 brfvrcld2 36296 nb3grpr 39466 ismgmhm 39887 isrnghm 39996 |
Copyright terms: Public domain | W3C validator |