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  2606  nelne2  2607  nssne1  3328  nssne2  3329  psssstr  3376  difsn  3846  iununi  4051  nnsucelrlem2  4426  nnsucelr  4429  nndisjeq  4430  sfinltfin  4536  mosubopt  4613  phialllem1  4617  nbrne1  4657  nbrne2  4658  chfnrn  5400  fnasrn  5418  ffnfv  5428  f1elima  5475  enprmaplem3  6079  taddc  6230  nclenn  6250  fnfreclem3  6320