![]() |
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 962 mpteq12f 4084 opelopabsb 4261 elrelimasn 4995 fvelrnb 5564 fmptco 5683 fconstfvm 5735 f1oiso 5827 canth 5829 mpoeq123 5934 dfoprab4f 6194 fmpox 6201 nnmword 6519 elfi 6970 ltmpig 7338 mul0eqap 8627 qreccl 9642 0fz1 10045 zmodid2 10352 divgcdcoprm0 12101 cnptoprest 13742 txrest 13779 cbvrald 14543 |
Copyright terms: Public domain | W3C validator |