![]() |
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 282 | 1 ⊢ ((𝜓 ∧ 𝜑) → 𝜃) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∧ wa 103 ↔ wb 104 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 |
This theorem depends on definitions: df-bi 116 |
This theorem is referenced by: syl2anbr 288 xordc1 1339 imainss 4890 xpexr2m 4916 funeu2 5085 imadiflem 5138 fnop 5162 ssimaex 5414 isosolem 5657 acexmidlem2 5703 fnovex 5736 cnvoprab 6061 smores3 6120 freccllem 6229 riinerm 6432 enq0sym 7141 peano5nnnn 7577 axcaucvglemres 7584 uzind3 9016 xrltnsym 9420 xsubge0 9505 0fz1 9666 seqf 10075 seq3f1oleml 10117 exp1 10140 expp1 10141 resqrexlemf1 10620 resqrexlemfp1 10621 clim2ser 10945 clim2ser2 10946 isermulc2 10948 summodclem3 10988 fisumss 11000 fsum3cvg3 11004 iserabs 11083 isumshft 11098 isumsplit 11099 geoisum1 11127 geoisum1c 11128 cvgratnnlemnexp 11132 cvgratz 11140 mertenslem2 11144 effsumlt 11196 efgt1p 11200 gcd0id 11462 lcmgcd 11552 lcmdvds 11553 lcmid 11554 isprm2lem 11590 ennnfonelemjn 11707 neipsm 12105 xmetpsmet 12297 comet 12427 metrest 12434 expcncf 12504 cvgcmp2nlemabs 12811 |
Copyright terms: Public domain | W3C validator |