|   | 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 223 | . 2 ⊢ (𝜑 → (𝜑 ↔ 𝜓)) | 
| 3 | 2 | ibi 267 | 1 ⊢ (𝜑 → 𝜓) | 
| Colors of variables: wff setvar class | 
| Syntax hints: → wi 4 ↔ wb 206 | 
| 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 207 | 
| This theorem is referenced by: elimh 1083 eusv2i 5394 relsnb 5812 ffdm 6765 ov 7577 ovg 7598 oacl 8573 nnacl 8649 elpm2r 8885 djuxpdom 10226 djufi 10227 cfcof 10314 hargch 10713 uzaddcl 12946 expcllem 14113 lcmfval 16658 lcmf0val 16659 mreunirn 17644 filunirn 23890 ustelimasn 24231 metustfbas 24570 zrtelqelz 26801 usgreqdrusgr 29586 pjini 31718 fzspl 32791 f1ocnt 32804 xrge0tsmsbi 33066 bnj983 34965 poimirlem16 37643 poimirlem19 37646 poimirlem25 37652 ac6s6 38179 fouriersw 46246 etransclem25 46274 ismea 46466 bits0oALTV 47668 uzlidlring 48151 linccl 48331 resinsnlem 48771 termc2 49148 | 
| Copyright terms: Public domain | W3C validator |