![]() |
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 284 | . 2 ⊢ ((𝜑 ∧ 𝜒) → 𝜃) |
5 | 1, 4 | sylan2b 287 | 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: sylancb 418 stdcndc 846 reupick3 3435 difprsnss 3745 trin2 5038 imadiflem 5314 fnun 5341 fco 5400 f1co 5452 foco 5467 f1oun 5500 f1oco 5503 eqfunfv 5639 ftpg 5721 issmo 6314 tfrlem5 6340 ener 6806 domtr 6812 unen 6843 xpdom2 6858 mapen 6875 pm54.43 7220 axpre-lttrn 7914 axpre-mulgt0 7917 zmulcl 9337 qaddcl 9667 qmulcl 9669 rpaddcl 9709 rpmulcl 9710 rpdivcl 9711 xrltnsym 9825 xrlttri3 9829 ge0addcl 10013 ge0mulcl 10014 ge0xaddcl 10015 expclzaplem 10578 expge0 10590 expge1 10591 hashfacen 10851 qredeu 12132 nn0gcdsq 12235 mul4sq 12429 cnovex 14173 iscn2 14177 txuni 14240 txcn 14252 lgsne0 14917 mul2sq 14941 |
Copyright terms: Public domain | W3C validator |