![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > sylan9bbr | GIF version |
Description: Nested syllogism inference conjoining dissimilar antecedents. (Contributed by NM, 4-Mar-1995.) |
Ref | Expression |
---|---|
sylan9bbr.1 | ⊢ (𝜑 → (𝜓 ↔ 𝜒)) |
sylan9bbr.2 | ⊢ (𝜃 → (𝜒 ↔ 𝜏)) |
Ref | Expression |
---|---|
sylan9bbr | ⊢ ((𝜃 ∧ 𝜑) → (𝜓 ↔ 𝜏)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | sylan9bbr.1 | . . 3 ⊢ (𝜑 → (𝜓 ↔ 𝜒)) | |
2 | sylan9bbr.2 | . . 3 ⊢ (𝜃 → (𝜒 ↔ 𝜏)) | |
3 | 1, 2 | sylan9bb 462 | . 2 ⊢ ((𝜑 ∧ 𝜃) → (𝜓 ↔ 𝜏)) |
4 | 3 | ancoms 268 | 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: pm5.75 964 mpteq12f 4109 opelopabsb 4290 elrelimasn 5031 fvelrnb 5604 fmptco 5724 fconstfvm 5776 f1oiso 5869 canth 5871 mpoeq123 5977 elovmporab 6118 elovmporab1w 6119 dfoprab4f 6246 fmpox 6253 nnmword 6571 elfi 7030 ltmpig 7399 mul0eqap 8689 qreccl 9707 0fz1 10111 zmodid2 10423 divgcdcoprm0 12239 cnptoprest 14407 txrest 14444 cbvrald 15280 |
Copyright terms: Public domain | W3C validator |