![]() |
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 133 | . 2 ⊢ (𝜑 → 𝜒) |
3 | sylan2br.2 | . 2 ⊢ ((𝜓 ∧ 𝜒) → 𝜃) | |
4 | 2, 3 | sylan2 286 | 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: syl2anbr 292 xordc1 1404 exmid1stab 4223 imainss 5059 xpexr2m 5085 funeu2 5258 imadiflem 5311 fnop 5335 ssimaex 5594 isosolem 5842 acexmidlem2 5889 fnovex 5925 cnvoprab 6254 smores3 6313 freccllem 6422 riinerm 6629 pw1fin 6933 enq0sym 7456 peano5nnnn 7916 axcaucvglemres 7923 uzind3 9391 xrltnsym 9818 xsubge0 9906 0fz1 10070 seqf 10487 seq3f1oleml 10529 exp1 10552 expp1 10553 resqrexlemf1 11044 resqrexlemfp1 11045 clim2ser 11372 clim2ser2 11373 isermulc2 11375 summodclem3 11415 fisumss 11427 fsum3cvg3 11431 iserabs 11510 isumshft 11525 isumsplit 11526 geoisum1 11554 geoisum1c 11555 cvgratnnlemnexp 11559 cvgratz 11567 mertenslem2 11571 clim2prod 11574 clim2divap 11575 fprodseq 11618 prodssdc 11624 fprodssdc 11625 effsumlt 11727 efgt1p 11731 gcd0id 12007 lcmgcd 12105 lcmdvds 12106 lcmid 12107 isprm2lem 12143 pcmpt 12370 ennnfonelemjn 12448 issgrpd 12868 mulg1 13062 srglmhm 13340 srgrmhm 13341 neipsm 14091 xmetpsmet 14306 comet 14436 metrest 14443 expcncf 14529 lgscllem 14845 lgsdir2 14871 lgsdirnn0 14885 lgsdinn0 14886 cvgcmp2nlemabs 15218 nconstwlpolem 15251 |
Copyright terms: Public domain | W3C validator |