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 12758 expcllem 13907 lcmfval 16432 lcmf0val 16433 mreunirn 17416 filunirn 23156 ustelimasn 23497 metustfbas 23836 usgreqdrusgr 28315 pjini 30440 fzspl 31488 f1ocnt 31500 xrge0tsmsbi 31695 bnj983 33337 poimirlem16 35990 poimirlem19 35993 poimirlem25 35999 ac6s6 36527 zrtelqelz 40700 fouriersw 44227 etransclem25 44255 ismea 44447 bits0oALTV 45628 uzlidlring 45982 linccl 46250 |
Copyright terms: Public domain | W3C validator |