![]() |
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 271 | . 2 ⊢ ((𝜑 ∧ 𝜃) → (𝜓 ↔ 𝜒)) |
3 | sylan9bb.2 | . . 3 ⊢ (𝜃 → (𝜒 ↔ 𝜏)) | |
4 | 3 | adantl 272 | . 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-1 5 ax-2 6 ax-mp 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 |
This theorem depends on definitions: df-bi 116 |
This theorem is referenced by: sylan9bbr 452 bi2anan9 574 baibd 873 rbaibd 874 syl3an9b 1253 sbcomxyyz 1901 eqeq12 2107 eleq12 2159 sbhypf 2682 ceqsrex2v 2763 sseq12 3064 rexprg 3514 rextpg 3516 breq12 3872 opelopabg 4119 brabg 4120 opelopab2 4121 ralxpf 4613 rexxpf 4614 feq23 5182 f00 5237 fconstg 5242 f1oeq23 5282 f1o00 5323 f1oiso 5643 riota1a 5665 cbvmpt2x 5764 caovord 5854 caovord3 5856 genpelvl 7168 genpelvu 7169 nn0ind-raph 8962 xnn0xadd0 9433 elfz 9579 elfzp12 9662 shftfibg 10385 shftfib 10388 absdvdsb 11257 dvdsabsb 11258 dvdsabseq 11291 tgss2 11947 lmbr 12080 xmetec 12239 |
Copyright terms: Public domain | W3C validator |