![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > biimtrrid | Unicode version |
Description: A mixed syllogism inference from a nested implication and a biconditional. (Contributed by NM, 5-Aug-1993.) |
Ref | Expression |
---|---|
biimtrrid.1 |
![]() ![]() ![]() ![]() ![]() ![]() |
biimtrrid.2 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
biimtrrid |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | biimtrrid.1 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() | |
2 | 1 | biimpri 133 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() |
3 | biimtrrid.2 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
4 | 2, 3 | syl5 32 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
Syntax hints: ![]() ![]() |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-ia2 107 ax-ia3 108 |
This theorem depends on definitions: df-bi 117 |
This theorem is referenced by: 3imtr3g 204 19.37-1 1674 mo3h 2079 necon1bidc 2399 necon4aidc 2415 r19.30dc 2624 ceqex 2864 ssdisj 3479 ralidm 3523 exmid1dc 4200 rexxfrd 4463 sucprcreg 4548 imain 5298 f0rn0 5410 funopfv 5555 mpteqb 5606 funfvima 5748 fliftfun 5796 iinerm 6606 eroveu 6625 th3qlem1 6636 updjudhf 7077 elni2 7312 genpdisj 7521 lttri3 8035 nn0ltexp2 10685 zfz1iso 10816 cau3lem 11118 maxleast 11217 rexanre 11224 climcau 11350 summodc 11386 mertenslem2 11539 prodmodclem2 11580 prodmodc 11581 fprodseq 11586 divgcdcoprmex 12096 prmind2 12114 pcqmul 12297 pcxcl 12305 pcadd 12333 mul4sq 12386 issubg2m 13002 dvdsrtr 13223 unitgrp 13238 subrgintm 13324 opnneiid 13557 txuni2 13649 txbas 13651 txbasval 13660 txlm 13672 blin2 13825 tgqioo 13940 2sqlem5 14348 bj-charfunr 14444 |
Copyright terms: Public domain | W3C validator |