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 159 | . 2 ⊢ (𝜒 → (𝜑 → 𝜓)) |
3 | 2 | imp 123 | 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: biantr 947 elrab3t 2885 difprsnss 3718 elpw2g 4142 elon2 4361 ideqg 4762 elrnmpt1s 4861 elrnmptg 4863 fun11iun 5463 eqfnfv2 5594 fmpt 5646 elunirn 5745 spc2ed 6212 tposfo2 6246 tposf12 6248 dom2lem 6750 enfii 6852 ac6sfi 6876 ltexprlemm 7562 elreal2 7792 fihasheqf1oi 10722 fprod2dlemstep 11585 bastop2 12878 |
Copyright terms: Public domain | W3C validator |