Theorem biimpcd 158

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

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

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

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  biimpac  296  3impexpbicom  1426  ax16  1801  ax16i  1846  nelneq  2267  nelneq2  2268  nelne1  2426  nelne2  2427  spc2gv  2817  spc3gv  2819  nssne1  3200  nssne2  3201  ifbothdc  3552  difsn  3710  iununir  3949  nbrne1  4001  nbrne2  4002  ss1o0el1  4176  mosubopt  4669  issref  4986  ssimaex  5547  chfnrn  5596  ffnfv  5643  f1elima  5741  dftpos4  6231  tfr1onlemsucaccv  6309  tfrcllemsucaccv  6322  snon0  6901  exmidonfinlem  7149  enq0sym  7373  prop  7416  prubl  7427  negf1o  8280  0fz1  9980  elfzmlbp  10067  maxleast  11155  negfi  11169  isprm2  12049  nprmdvds1  12072  oddprmdvds  12284  exmidsbthrlem  13901