Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > syl5bir | Unicode version |
Description: A mixed syllogism inference from a nested implication and a biconditional. (Contributed by NM, 5-Aug-1993.) |
Ref | Expression |
---|---|
syl5bir.1 | |
syl5bir.2 |
Ref | Expression |
---|---|
syl5bir |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | syl5bir.1 | . . 3 | |
2 | 1 | biimpri 132 | . 2 |
3 | syl5bir.2 | . 2 | |
4 | 2, 3 | syl5 32 | 1 |
Colors of variables: wff set class |
Syntax hints: wi 4 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: 3imtr3g 203 19.37-1 1637 mo3h 2030 necon1bidc 2337 necon4aidc 2353 ceqex 2786 ssdisj 3389 ralidm 3433 exmid1dc 4093 rexxfrd 4354 sucprcreg 4434 imain 5175 f0rn0 5287 funopfv 5429 mpteqb 5479 funfvima 5617 fliftfun 5665 iinerm 6469 eroveu 6488 th3qlem1 6499 updjudhf 6932 elni2 7090 genpdisj 7299 lttri3 7812 zfz1iso 10552 cau3lem 10854 maxleast 10953 rexanre 10960 climcau 11084 summodc 11120 mertenslem2 11273 divgcdcoprmex 11710 prmind2 11728 opnneiid 12260 txuni2 12352 txbas 12354 txbasval 12363 txlm 12375 blin2 12528 tgqioo 12643 |
Copyright terms: Public domain | W3C validator |