![]() |
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 276 | . 2 ⊢ ((𝜑 ∧ 𝜃) → (𝜓 ↔ 𝜒)) |
3 | sylan9bb.2 | . . 3 ⊢ (𝜃 → (𝜒 ↔ 𝜏)) | |
4 | 3 | adantl 277 | . 2 ⊢ ((𝜑 ∧ 𝜃) → (𝜒 ↔ 𝜏)) |
5 | 2, 4 | bitrd 188 | 1 ⊢ ((𝜑 ∧ 𝜃) → (𝜓 ↔ 𝜏)) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∧ wa 104 ↔ wb 105 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-ia2 107 ax-ia3 108 |
This theorem depends on definitions: df-bi 117 |
This theorem is referenced by: sylan9bbr 463 bi2anan9 606 baibd 923 rbaibd 924 syl3an9b 1310 sbcomxyyz 1972 eqeq12 2190 eleq12 2242 sbhypf 2788 ceqsrex2v 2871 sseq12 3182 rexprg 3646 rextpg 3648 breq12 4010 opelopabg 4270 brabg 4271 opelopab2 4272 ralxpf 4775 rexxpf 4776 feq23 5353 f00 5409 fconstg 5414 f1oeq23 5454 f1o00 5498 f1oiso 5829 riota1a 5852 cbvmpox 5955 caovord 6048 caovord3 6050 rbropapd 6245 genpelvl 7513 genpelvu 7514 nn0ind-raph 9372 elpq 9650 xnn0xadd0 9869 elfz 10016 elfzp12 10101 shftfibg 10831 shftfib 10834 absdvdsb 11818 dvdsabsb 11819 dvdsabseq 11855 islmod 13386 tgss2 13664 lmbr 13798 xmetec 14022 |
Copyright terms: Public domain | W3C validator |