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  711  elpr2  3691  eusv2i  4552  ffdm  5505  ov  6140  ovg  6160  nnacl  6647  elpm2r  6834  ltnqpri  7813  ltxrlt  8244  uzaddcl  9819  expcllem  10811  qexpclz  10821  1exp  10829  facnn  10988  fac0  10989  fac1  10990  bcn2  11025  en1hash  11061  hash2en  11106  znnen  13018  zrhval  14630