![]() |
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 831 rbaibd 832 syl3an9b 1204 sbcomxyyz 1843 eqeq12 2049 eleq12 2099 sbhypf 2597 ceqsrex2v 2670 sseq12 2962 rexprg 3413 rextpg 3415 breq12 3760 opelopabg 3996 brabg 3997 opelopab2 3998 ralxpf 4425 rexxpf 4426 feq23 4976 f00 5024 fconstg 5026 f1oeq23 5063 f1o00 5104 f1oiso 5408 riota1a 5430 cbvmpt2x 5524 caovord 5614 caovord3 5616 genpelvl 6495 genpelvu 6496 nn0ind-raph 8131 elfz 8650 elfzp12 8731 |
Copyright terms: Public domain | W3C validator |