Theorem ibir 177

Description: Inference that converts a biconditional implied by one of its arguments, into an implication. (Contributed by NM, 22-Jul-2004.)

Hypothesis

Ref	Expression
ibir.1	⊢ (𝜑 → (𝜓 ↔ 𝜑))

Assertion

Ref	Expression
ibir	⊢ (𝜑 → 𝜓)

Proof of Theorem ibir

Step	Hyp	Ref	Expression
1		ibir.1	. . 3 ⊢ (𝜑 → (𝜓 ↔ 𝜑))
2	1	bicomd 141	. 2 ⊢ (𝜑 → (𝜑 ↔ 𝜓))
3	2	ibi 176	1 ⊢ (𝜑 → 𝜓)

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  709  elpr2  3688  eusv2i  4545  ffdm  5493  ov  6123  ovg  6143  nnacl  6624  elpm2r  6811  ltnqpri  7777  ltxrlt  8208  uzaddcl  9777  expcllem  10767  qexpclz  10777  1exp  10785  facnn  10944  fac0  10945  fac1  10946  bcn2  10981  hash2en  11060  znnen  12964  zrhval  14575