Theorem biimpcd 215

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	|- (ph -> (ps <-> ch))

Assertion

Ref	Expression
biimpcd	|- (ps -> (ph -> ch))

Proof of Theorem biimpcd

Step	Hyp	Ref	Expression
1		id 19	. 2 |- (ps -> ps)
2		biimpcd.1	. 2 |- (ph -> (ps <-> ch))
3	1, 2	syl5ibcom 211	1 |- (ps -> (ph -> ch))

Syntax hints:   -> wi 4   <-> wb 176

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 177

This theorem is referenced by:  biimpac  472  3impexpbicom  1367  ax16i  2046  ax16ALT2  2048  nfsb4t  2080  nelneq  2451  nelneq2  2452  nelne1  2605  nelne2  2606  nssne1  3327  nssne2  3328  psssstr  3375  difsn  3845  iununi  4050  nnsucelrlem2  4425  nnsucelr  4428  nndisjeq  4429  sfinltfin  4535  mosubopt  4612  phialllem1  4616  nbrne1  4656  nbrne2  4657  chfnrn  5399  fnasrn  5417  ffnfv  5427  f1elima  5474  enprmaplem3  6078  taddc  6229  nclenn  6249  fnfreclem3  6319