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 921 elrab3t 2812 difprsnss 3628 elpw2g 4051 elon2 4268 ideqg 4660 elrnmpt1s 4759 elrnmptg 4761 fun11iun 5356 eqfnfv2 5487 fmpt 5538 elunirn 5635 spc2ed 6098 tposfo2 6132 tposf12 6134 dom2lem 6634 enfii 6736 ac6sfi 6760 ltexprlemm 7376 elreal2 7606 fihasheqf1oi 10502 bastop2 12180 |
Copyright terms: Public domain | W3C validator |