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  712  elpr2  3711  eusv2i  4576  ffdm  5533  ov  6173  ovg  6193  nnacl  6713  elpm2r  6900  ltnqpri  7909  ltxrlt  8339  uzaddcl  9918  expcllem  10912  qexpclz  10922  1exp  10930  facnn  11089  fac0  11090  fac1  11091  bcn2  11126  en1hash  11163  hash2en  11215  znnen  13149  zrhval  14765