![]() |
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 261 | . 2 ⊢ ((𝜑 ∧ 𝜃) → (𝜓 ↔ 𝜒)) |
3 | sylan9bb.2 | . . 3 ⊢ (𝜃 → (𝜒 ↔ 𝜏)) | |
4 | 3 | adantl 262 | . 2 ⊢ ((𝜑 ∧ 𝜃) → (𝜒 ↔ 𝜏)) |
5 | 2, 4 | bitrd 177 | 1 ⊢ ((𝜑 ∧ 𝜃) → (𝜓 ↔ 𝜏)) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∧ wa 97 ↔ wb 98 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 99 ax-ia2 100 ax-ia3 101 |
This theorem depends on definitions: df-bi 110 |
This theorem is referenced by: sylan9bbr 436 bi2anan9 538 baibd 832 rbaibd 833 syl3an9b 1205 sbcomxyyz 1846 eqeq12 2052 eleq12 2102 sbhypf 2603 ceqsrex2v 2676 sseq12 2968 rexprg 3422 rextpg 3424 breq12 3769 opelopabg 4005 brabg 4006 opelopab2 4007 ralxpf 4482 rexxpf 4483 feq23 5033 f00 5081 fconstg 5083 f1oeq23 5120 f1o00 5161 f1oiso 5465 riota1a 5487 cbvmpt2x 5582 caovord 5672 caovord3 5674 genpelvl 6610 genpelvu 6611 nn0ind-raph 8355 elfz 8880 elfzp12 8961 shftfibg 9421 shftfib 9424 |
Copyright terms: Public domain | W3C validator |