Theorem ibir 176

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 140	. 2 ⊢ (𝜑 → (𝜑 ↔ 𝜓))
3	2	ibi 175	1 ⊢ (𝜑 → 𝜓)

Syntax hints:   → wi 4   ↔ wb 104

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  pm5.21nii  656  elpr2  3472  eusv2i  4290  ffdm  5194  ov  5778  ovg  5797  nnacl  6255  elpm2r  6437  ltnqpri  7214  ltxrlt  7613  uzaddcl  9135  expcllem  10027  qexpclz  10037  1exp  10045  facnn  10196  fac0  10197  fac1  10198  bcn2  10233  znnen  11550