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 ⊢ (𝜑 → 𝜓)

This proof depends on syntax axioms:   → wi 4   ↔ wb 105

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This proof depends on definitions:  df-bi 117

This theorem is used by:  pm5.21nii  716  elpr2  3731  eusv2i  4601  ffdm  5558  ov  6208  ovg  6228  nnacl  6753  elpm2r  6940  ltnqpri  7962  ltxrlt  8392  uzaddcl  9996  fzspl  10487  expcllem  11002  qexpclz  11012  1exp  11020  facnn  11181  fac0  11182  fac1  11183  bcn2  11218  en1hash  11255  hash2en  11311  znnen  13341  zrhval  15036