![]() |
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 8021 uzaddcl 9584 expcllem 10528 qexpclz 10538 1exp 10546 facnn 10702 fac0 10703 fac1 10704 bcn2 10739 znnen 12393 |
Copyright terms: Public domain | W3C validator |