![]() |
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 3615 eusv2i 4456 ffdm 5387 ov 5994 ovg 6013 nnacl 6481 elpm2r 6666 ltnqpri 7593 ltxrlt 8023 uzaddcl 9586 expcllem 10531 qexpclz 10541 1exp 10549 facnn 10707 fac0 10708 fac1 10709 bcn2 10744 znnen 12399 |
Copyright terms: Public domain | W3C validator |