| 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 4123 opelopabsb 4305 elrelimasn 5047 fvelrnb 5625 fmptco 5745 fconstfvm 5801 f1oiso 5894 canth 5896 mpoeq123 6003 elovmporab 6145 elovmporab1w 6146 dfoprab4f 6278 fmpox 6285 nnmword 6603 elfi 7072 ltmpig 7451 mul0eqap 8742 qreccl 9762 0fz1 10166 zmodid2 10495 divgcdcoprm0 12394 cnptoprest 14682 txrest 14719 cbvrald 15686 |
| Copyright terms: Public domain | W3C validator |