|   | 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 1082 eusv2i 5393 relsnb 5811 ffdm 6764 ov 7578 ovg 7599 oacl 8574 nnacl 8650 elpm2r 8886 djuxpdom 10227 djufi 10228 cfcof 10315 hargch 10714 uzaddcl 12947 expcllem 14114 lcmfval 16659 lcmf0val 16660 mreunirn 17645 filunirn 23891 ustelimasn 24232 metustfbas 24571 zrtelqelz 26802 usgreqdrusgr 29587 pjini 31719 fzspl 32792 f1ocnt 32805 xrge0tsmsbi 33067 bnj983 34966 poimirlem16 37644 poimirlem19 37647 poimirlem25 37653 ac6s6 38180 fouriersw 46251 etransclem25 46279 ismea 46471 bits0oALTV 47673 uzlidlring 48156 linccl 48336 resinsnlem 48777 termc2 49176 discsntermlem 49222 | 
| Copyright terms: Public domain | W3C validator |