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  2883  undif4  3607  sneqbg  3875  adj11  3889  elpwuni  4053  opkthg  4131  iotanul  4354  preaddccan2  4455  suc11nnc  4558  phialllem1  4616  ssxpb  5055  xp11  5056  xpcan  5057  xpcan2  5058  imadif  5171  2elresin  5194  f1fveq  5473  f1elima  5474  enpw1  6062  peano4nc  6150  addceq0  6219  ce0tb  6238  addccan2nc  6265