![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > ibir | GIF version |
Description: Inference that converts a biconditional implied by one of its arguments, into an implication. (Contributed by NM, 22-Jul-2004.) |
Ref | Expression |
---|---|
ibir.1 | ⊢ (𝜑 → (𝜓 ↔ 𝜑)) |
Ref | Expression |
---|---|
ibir | ⊢ (𝜑 → 𝜓) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ibir.1 | . . 3 ⊢ (𝜑 → (𝜓 ↔ 𝜑)) | |
2 | 1 | bicomd 141 | . 2 ⊢ (𝜑 → (𝜑 ↔ 𝜓)) |
3 | 2 | ibi 176 | 1 ⊢ (𝜑 → 𝜓) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ↔ 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: pm5.21nii 704 elpr2 3614 eusv2i 4455 ffdm 5386 ov 5993 ovg 6012 nnacl 6480 elpm2r 6665 ltnqpri 7592 ltxrlt 8022 uzaddcl 9585 expcllem 10530 qexpclz 10540 1exp 10548 facnn 10706 fac0 10707 fac1 10708 bcn2 10743 znnen 12398 |
Copyright terms: Public domain | W3C validator |