![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > syl2anb | GIF version |
Description: A double syllogism inference. (Contributed by NM, 29-Jul-1999.) |
Ref | Expression |
---|---|
syl2anb.1 | ⊢ (𝜑 ↔ 𝜓) |
syl2anb.2 | ⊢ (𝜏 ↔ 𝜒) |
syl2anb.3 | ⊢ ((𝜓 ∧ 𝜒) → 𝜃) |
Ref | Expression |
---|---|
syl2anb | ⊢ ((𝜑 ∧ 𝜏) → 𝜃) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | syl2anb.2 | . 2 ⊢ (𝜏 ↔ 𝜒) | |
2 | syl2anb.1 | . . 3 ⊢ (𝜑 ↔ 𝜓) | |
3 | syl2anb.3 | . . 3 ⊢ ((𝜓 ∧ 𝜒) → 𝜃) | |
4 | 2, 3 | sylanb 280 | . 2 ⊢ ((𝜑 ∧ 𝜒) → 𝜃) |
5 | 1, 4 | sylan2b 283 | 1 ⊢ ((𝜑 ∧ 𝜏) → 𝜃) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∧ wa 103 ↔ wb 104 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 |
This theorem depends on definitions: df-bi 116 |
This theorem is referenced by: sylancb 412 stdcndc 813 reupick3 3325 difprsnss 3622 trin2 4886 imadiflem 5158 fnun 5185 fco 5244 f1co 5296 foco 5311 f1oun 5341 f1oco 5344 eqfunfv 5475 ftpg 5556 issmo 6137 tfrlem5 6163 ener 6625 domtr 6631 unen 6662 xpdom2 6676 mapen 6691 pm54.43 6993 axpre-lttrn 7613 axpre-mulgt0 7616 zmulcl 9005 qaddcl 9323 qmulcl 9325 rpaddcl 9360 rpmulcl 9361 rpdivcl 9362 xrltnsym 9466 xrlttri3 9470 ge0addcl 9651 ge0mulcl 9652 ge0xaddcl 9653 expclzaplem 10204 expge0 10216 expge1 10217 hashfacen 10466 qredeu 11618 nn0gcdsq 11717 iscn2 12205 txuni 12268 txcn 12280 |
Copyright terms: Public domain | W3C validator |