Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > ibir | Structured version Visualization version 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 222 | . 2 ⊢ (𝜑 → (𝜑 ↔ 𝜓)) |
3 | 2 | ibi 267 | 1 ⊢ (𝜑 → 𝜓) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 205 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 |
This theorem depends on definitions: df-bi 206 |
This theorem is referenced by: elimh 1084 eusv2i 5348 relsnb 5755 ffdm 6694 ov 7492 ovg 7512 oacl 8449 nnacl 8526 elpm2r 8717 djuxpdom 10055 djufi 10056 cfcof 10144 hargch 10543 uzaddcl 12759 expcllem 13908 lcmfval 16433 lcmf0val 16434 mreunirn 17417 filunirn 23161 ustelimasn 23502 metustfbas 23841 usgreqdrusgr 28321 pjini 30446 fzspl 31494 f1ocnt 31506 xrge0tsmsbi 31701 bnj983 33343 poimirlem16 36025 poimirlem19 36028 poimirlem25 36034 ac6s6 36562 zrtelqelz 40733 fouriersw 44263 etransclem25 44291 ismea 44483 bits0oALTV 45664 uzlidlring 46018 linccl 46286 |
Copyright terms: Public domain | W3C validator |