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 1371 imainss 4949 xpexr2m 4975 funeu2 5144 imadiflem 5197 fnop 5221 ssimaex 5475 isosolem 5718 acexmidlem2 5764 fnovex 5797 cnvoprab 6124 smores3 6183 freccllem 6292 riinerm 6495 enq0sym 7233 peano5nnnn 7693 axcaucvglemres 7700 uzind3 9157 xrltnsym 9572 xsubge0 9657 0fz1 9818 seqf 10227 seq3f1oleml 10269 exp1 10292 expp1 10293 resqrexlemf1 10773 resqrexlemfp1 10774 clim2ser 11099 clim2ser2 11100 isermulc2 11102 summodclem3 11142 fisumss 11154 fsum3cvg3 11158 iserabs 11237 isumshft 11252 isumsplit 11253 geoisum1 11281 geoisum1c 11282 cvgratnnlemnexp 11286 cvgratz 11294 mertenslem2 11298 clim2prod 11301 clim2divap 11302 effsumlt 11387 efgt1p 11391 gcd0id 11656 lcmgcd 11748 lcmdvds 11749 lcmid 11750 isprm2lem 11786 ennnfonelemjn 11904 neipsm 12312 xmetpsmet 12527 comet 12657 metrest 12664 expcncf 12750 exmid1stab 13184 cvgcmp2nlemabs 13216 |
Copyright terms: Public domain | W3C validator |