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 132 | . 2 ⊢ (𝜑 → 𝜒) |
3 | sylan2br.2 | . 2 ⊢ ((𝜓 ∧ 𝜒) → 𝜃) | |
4 | 2, 3 | sylan2 284 | 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: syl2anbr 290 xordc1 1356 imainss 4924 xpexr2m 4950 funeu2 5119 imadiflem 5172 fnop 5196 ssimaex 5450 isosolem 5693 acexmidlem2 5739 fnovex 5772 cnvoprab 6099 smores3 6158 freccllem 6267 riinerm 6470 enq0sym 7208 peano5nnnn 7668 axcaucvglemres 7675 uzind3 9132 xrltnsym 9547 xsubge0 9632 0fz1 9793 seqf 10202 seq3f1oleml 10244 exp1 10267 expp1 10268 resqrexlemf1 10748 resqrexlemfp1 10749 clim2ser 11074 clim2ser2 11075 isermulc2 11077 summodclem3 11117 fisumss 11129 fsum3cvg3 11133 iserabs 11212 isumshft 11227 isumsplit 11228 geoisum1 11256 geoisum1c 11257 cvgratnnlemnexp 11261 cvgratz 11269 mertenslem2 11273 effsumlt 11325 efgt1p 11329 gcd0id 11594 lcmgcd 11686 lcmdvds 11687 lcmid 11688 isprm2lem 11724 ennnfonelemjn 11842 neipsm 12250 xmetpsmet 12465 comet 12595 metrest 12602 expcncf 12688 exmid1stab 13122 cvgcmp2nlemabs 13154 |
Copyright terms: Public domain | W3C validator |