Theorem impbid1 194

Description: Infer an equivalence from two implications. (Contributed by NM, 6-Mar-2007.)

Hypotheses

Ref	Expression
impbid1.1	|- (ph -> (ps -> ch))
impbid1.2	|- (ch -> ps)

Assertion

Ref	Expression
impbid1	|- (ph -> (ps <-> ch))

Proof of Theorem impbid1

Step	Hyp	Ref	Expression
1		impbid1.1	. 2 |- (ph -> (ps -> ch))
2		impbid1.2	. . 3 |- (ch -> ps)
3	2	a1i 10	. 2 |- (ph -> (ch -> ps))
4	1, 3	impbid 183	1 |- (ph -> (ps <-> 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:  impbid2  195  iba  489  ibar  490  pm5.71  902  cad0  1400  19.33b  1608  19.9t  1779  19.9tOLD  1857  a16gb  2050  sb4b  2054  eupickbi  2270  euor2  2272  2eu1  2284  2eu3  2286  ceqsalg  2884  undif4  3608  sneqbg  3876  adj11  3890  elpwuni  4054  opkthg  4132  iotanul  4355  preaddccan2  4456  suc11nnc  4559  phialllem1  4617  ssxpb  5056  xp11  5057  xpcan  5058  xpcan2  5059  imadif  5172  2elresin  5195  f1fveq  5474  f1elima  5475  enpw1  6063  peano4nc  6151  addceq0  6220  ce0tb  6239  addccan2nc  6266