Theorem biimpcd 148

Description: Deduce a commuted implication from a logical equivalence. (Contributed by NM, 3-May-1994.) (Proof shortened by Wolf Lammen, 22-Sep-2013.)

Hypothesis

Ref	Expression
biimpcd.1	⊢ (𝜑 → (𝜓 ↔ 𝜒))

Assertion

Ref	Expression
biimpcd	⊢ (𝜓 → (𝜑 → 𝜒))

Proof of Theorem biimpcd

Step	Hyp	Ref	Expression
1		id 19	. 2 ⊢ (𝜓 → 𝜓)
2		biimpcd.1	. 2 ⊢ (𝜑 → (𝜓 ↔ 𝜒))
3	1, 2	syl5ibcom 144	1 ⊢ (𝜓 → (𝜑 → 𝜒))

Syntax hints:   → wi 4   ↔ wb 98

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99

This theorem depends on definitions:  df-bi 110

This theorem is referenced by:  biimpac  282  3impexpbicom  1327  ax16  1694  ax16i  1738  nelneq  2138  nelneq2  2139  nelne1  2295  nelne2  2296  spc2gv  2643  spc3gv  2645  nssne1  3001  nssne2  3002  ifbothdc  3357  difsn  3501  iununir  3738  nbrne1  3781  nbrne2  3782  mosubopt  4405  issref  4707  ssimaex  5234  chfnrn  5278  ffnfv  5323  f1elima  5412  dftpos4  5878  snon0  6356  enq0sym  6530  prop  6573  prubl  6584  0fz1  8909  elfzmlbp  8990