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 3635 rextpg 3637 breq12 3994 opelopabg 4253 brabg 4254 opelopab2 4255 ralxpf 4757 rexxpf 4758 feq23 5333 f00 5389 fconstg 5394 f1oeq23 5434 f1o00 5477 f1oiso 5805 riota1a 5828 cbvmpox 5931 caovord 6024 caovord3 6026 rbropapd 6221 genpelvl 7474 genpelvu 7475 nn0ind-raph 9329 elpq 9607 xnn0xadd0 9824 elfz 9971 elfzp12 10055 shftfibg 10784 shftfib 10787 absdvdsb 11771 dvdsabsb 11772 dvdsabseq 11807 tgss2 12873 lmbr 13007 xmetec 13231 |
Copyright terms: Public domain | W3C validator |