![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > biimtrrid | GIF 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: → wi 4 ↔ wb 105 |
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 1685 mo3h 2095 necon1bidc 2416 necon4aidc 2432 r19.30dc 2641 ceqex 2887 ssdisj 3503 ralidm 3547 exmid1dc 4229 rexxfrd 4494 sucprcreg 4581 imain 5336 f0rn0 5448 funopfv 5596 mpteqb 5648 funfvima 5790 fliftfun 5839 iinerm 6661 eroveu 6680 th3qlem1 6691 updjudhf 7138 elni2 7374 genpdisj 7583 lttri3 8099 seqf1og 10592 nn0ltexp2 10780 zfz1iso 10912 cau3lem 11258 maxleast 11357 rexanre 11364 climcau 11490 summodc 11526 mertenslem2 11679 prodmodclem2 11720 prodmodc 11721 fprodseq 11726 divgcdcoprmex 12240 prmind2 12258 pcqmul 12441 pcxcl 12449 pcadd 12478 mul4sq 12532 issubg2m 13259 dvdsrtr 13597 unitgrp 13612 subrgintm 13739 islssm 13853 znidom 14145 opnneiid 14332 txuni2 14424 txbas 14426 txbasval 14435 txlm 14447 blin2 14600 tgqioo 14715 plyadd 14897 plymul 14898 2sqlem5 15206 bj-charfunr 15302 |
Copyright terms: Public domain | W3C validator |