Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > sylan9bb | GIF version |
Description: Nested syllogism inference conjoining dissimilar antecedents. (Contributed by NM, 4-Mar-1995.) |
Ref | Expression |
---|---|
sylan9bb.1 | ⊢ (𝜑 → (𝜓 ↔ 𝜒)) |
sylan9bb.2 | ⊢ (𝜃 → (𝜒 ↔ 𝜏)) |
Ref | Expression |
---|---|
sylan9bb | ⊢ ((𝜑 ∧ 𝜃) → (𝜓 ↔ 𝜏)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | sylan9bb.1 | . . 3 ⊢ (𝜑 → (𝜓 ↔ 𝜒)) | |
2 | 1 | adantr 274 | . 2 ⊢ ((𝜑 ∧ 𝜃) → (𝜓 ↔ 𝜒)) |
3 | sylan9bb.2 | . . 3 ⊢ (𝜃 → (𝜒 ↔ 𝜏)) | |
4 | 3 | adantl 275 | . 2 ⊢ ((𝜑 ∧ 𝜃) → (𝜒 ↔ 𝜏)) |
5 | 2, 4 | bitrd 187 | 1 ⊢ ((𝜑 ∧ 𝜃) → (𝜓 ↔ 𝜏)) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∧ 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: sylan9bbr 460 bi2anan9 601 baibd 918 rbaibd 919 syl3an9b 1305 sbcomxyyz 1965 eqeq12 2183 eleq12 2235 sbhypf 2779 ceqsrex2v 2862 sseq12 3172 rexprg 3633 rextpg 3635 breq12 3992 opelopabg 4251 brabg 4252 opelopab2 4253 ralxpf 4755 rexxpf 4756 feq23 5331 f00 5387 fconstg 5392 f1oeq23 5432 f1o00 5475 f1oiso 5802 riota1a 5825 cbvmpox 5928 caovord 6021 caovord3 6023 rbropapd 6218 genpelvl 7461 genpelvu 7462 nn0ind-raph 9316 elpq 9594 xnn0xadd0 9811 elfz 9958 elfzp12 10042 shftfibg 10771 shftfib 10774 absdvdsb 11758 dvdsabsb 11759 dvdsabseq 11794 tgss2 12832 lmbr 12966 xmetec 13190 |
Copyright terms: Public domain | W3C validator |