Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > syl5bir | GIF 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 1661 mo3h 2066 necon1bidc 2386 necon4aidc 2402 r19.30dc 2611 ceqex 2848 ssdisj 3460 ralidm 3504 exmid1dc 4173 rexxfrd 4435 sucprcreg 4520 imain 5264 f0rn0 5376 funopfv 5520 mpteqb 5570 funfvima 5710 fliftfun 5758 iinerm 6564 eroveu 6583 th3qlem1 6594 updjudhf 7035 elni2 7246 genpdisj 7455 lttri3 7969 nn0ltexp2 10612 zfz1iso 10740 cau3lem 11042 maxleast 11141 rexanre 11148 climcau 11274 summodc 11310 mertenslem2 11463 prodmodclem2 11504 prodmodc 11505 fprodseq 11510 divgcdcoprmex 12013 prmind2 12031 pcqmul 12214 pcxcl 12222 pcadd 12250 opnneiid 12711 txuni2 12803 txbas 12805 txbasval 12814 txlm 12826 blin2 12979 tgqioo 13094 bj-charfunr 13533 |
Copyright terms: Public domain | W3C validator |