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 457 | . 2 ⊢ ((𝜑 ∧ 𝜃) → (𝜓 ↔ 𝜏)) |
4 | 3 | ancoms 266 | 1 ⊢ ((𝜃 ∧ 𝜑) → (𝜓 ↔ 𝜏)) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∧ wa 103 ↔ wb 104 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 |
This theorem depends on definitions: df-bi 116 |
This theorem is referenced by: pm5.75 946 mpteq12f 4008 opelopabsb 4182 elreimasng 4905 fvelrnb 5469 fmptco 5586 fconstfvm 5638 f1oiso 5727 mpoeq123 5830 dfoprab4f 6091 fmpox 6098 nnmword 6414 elfi 6859 ltmpig 7147 mul0eqap 8431 qreccl 9434 0fz1 9825 zmodid2 10125 divgcdcoprm0 11782 cnptoprest 12408 txrest 12445 cbvrald 12995 |
Copyright terms: Public domain | W3C validator |