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  6141  ovg  6161  nnacl  6648  elpm2r  6835  ltnqpri  7814  ltxrlt  8245  uzaddcl  9820  expcllem  10813  qexpclz  10823  1exp  10831  facnn  10990  fac0  10991  fac1  10992  bcn2  11027  en1hash  11063  hash2en  11108  znnen  13024  zrhval  14637