Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > mpbiran2 | Unicode version |
Description: Detach truth from conjunction in biconditional. (Contributed by NM, 22-Feb-1996.) (Revised by NM, 9-Jan-2015.) |
Ref | Expression |
---|---|
mpbiran2.1 | |
mpbiran2.2 |
Ref | Expression |
---|---|
mpbiran2 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | mpbiran2.2 | . 2 | |
2 | mpbiran2.1 | . . 3 | |
3 | 2 | biantru 300 | . 2 |
4 | 1, 3 | bitr4i 186 | 1 |
Colors of variables: wff set class |
Syntax hints: wa 103 wb 104 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 |
This theorem depends on definitions: df-bi 116 |
This theorem is referenced by: reueq 2878 ss0b 3397 eusv1 4368 eusv2nf 4372 eusv2 4373 opthprc 4585 opelres 4819 f1cnvcnv 5334 fores 5349 f1orn 5370 funfvdm 5477 dfoprab2 5811 tpostpos 6154 opelreal 7628 elreal2 7631 eqresr 7637 axprecex 7681 zeoxor 11555 isprm2 11787 toptopon 12174 bdeq0 13054 subctctexmid 13185 |
Copyright terms: Public domain | W3C validator |