![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > biimparc | GIF version |
Description: Inference from a logical equivalence. (Contributed by NM, 3-May-1994.) |
Ref | Expression |
---|---|
biimpa.1 | ⊢ (𝜑 → (𝜓 ↔ 𝜒)) |
Ref | Expression |
---|---|
biimparc | ⊢ ((𝜒 ∧ 𝜑) → 𝜓) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | biimpa.1 | . . 3 ⊢ (𝜑 → (𝜓 ↔ 𝜒)) | |
2 | 1 | biimprcd 160 | . 2 ⊢ (𝜒 → (𝜑 → 𝜓)) |
3 | 2 | imp 124 | 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: biantr 954 elrab3t 2907 difprsnss 3745 elpw2g 4174 elon2 4394 ideqg 4796 elrnmpt1s 4895 elrnmptg 4897 fun11iun 5501 eqfnfv2 5635 fmpt 5687 elunirn 5788 spc2ed 6259 tposfo2 6293 tposf12 6295 dom2lem 6799 enfii 6903 ac6sfi 6927 ltexprlemm 7630 elreal2 7860 fihasheqf1oi 10802 fprod2dlemstep 11665 bastop2 14061 |
Copyright terms: Public domain | W3C validator |