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 665 | . 2 |
3 | biadan2.2 | . . 3 | |
4 | 3 | pm5.32i 669 | . 2 |
5 | 2, 4 | bitri 264 | 1 |
Colors of variables: wff setvar class |
Syntax hints: wi 4 wb 196 wa 384 |
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 197 df-an 386 |
This theorem is referenced by: elab4g 3355 elpwb 4169 brab2a 5194 elon2 5734 elovmpt2 6879 eqop2 7209 iscard 8801 iscard2 8802 elnnnn0 11336 elfzo2 12473 bitsval 15146 1nprm 15392 funcpropd 16560 isfull 16570 isfth 16574 ismhm 17337 isghm 17660 ghmpropd 17698 isga 17724 oppgcntz 17794 gexdvdsi 17998 isrhm 18721 abvpropd 18842 islmhm 19027 dfprm2 19842 prmirred 19843 elocv 20012 isobs 20064 iscn2 21042 iscnp2 21043 islocfin 21320 elflim2 21768 isfcls 21813 isnghm 22527 isnmhm 22550 0plef 23439 elply 23951 dchrelbas4 24968 nb3grpr 26284 ispligb 27329 isph 27677 abfmpunirn 29452 iscvm 31241 brsslt 31900 sscoid 32020 bj-ismoorec 33060 eldiophb 37320 eldioph3b 37328 eldioph4b 37375 issdrg 37767 brfvrcld2 37984 ismgmhm 41783 isrnghm 41892 |
Copyright terms: Public domain | W3C validator |