![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > sylan2br | GIF version |
Description: A syllogism inference. (Contributed by NM, 21-Apr-1994.) |
Ref | Expression |
---|---|
sylan2br.1 | ⊢ (𝜒 ↔ 𝜑) |
sylan2br.2 | ⊢ ((𝜓 ∧ 𝜒) → 𝜃) |
Ref | Expression |
---|---|
sylan2br | ⊢ ((𝜓 ∧ 𝜑) → 𝜃) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | sylan2br.1 | . . 3 ⊢ (𝜒 ↔ 𝜑) | |
2 | 1 | biimpri 131 | . 2 ⊢ (𝜑 → 𝜒) |
3 | sylan2br.2 | . 2 ⊢ ((𝜓 ∧ 𝜒) → 𝜃) | |
4 | 2, 3 | sylan2 280 | 1 ⊢ ((𝜓 ∧ 𝜑) → 𝜃) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∧ wa 102 ↔ wb 103 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 104 ax-ia2 105 ax-ia3 106 |
This theorem depends on definitions: df-bi 115 |
This theorem is referenced by: syl2anbr 286 xordc1 1325 imainss 4769 xpexr2m 4792 funeu2 4957 imadiflem 5009 fnop 5033 ssimaex 5266 isosolem 5494 acexmidlem2 5540 fnovex 5569 cnvoprab 5886 smores3 5942 freccllem 6051 riinerm 6245 enq0sym 6684 peano5nnnn 7120 axcaucvglemres 7127 uzind3 8541 xrltnsym 8944 0fz1 9140 iseqfcl 9535 iseqfclt 9536 expivallem 9574 expival 9575 exp1 9579 expp1 9580 resqrexlemf1 10032 resqrexlemfp1 10033 clim2iser 10313 clim2iser2 10314 iisermulc2 10316 iserile 10318 climserile 10321 gcd0id 10514 lcmgcd 10604 lcmdvds 10605 lcmid 10606 isprm2lem 10642 |
Copyright terms: Public domain | W3C validator |