Theorem impbid2 195

Description: Infer an equivalence from two implications. (Contributed by NM, 6-Mar-2007.) (Proof shortened by Wolf Lammen, 27-Sep-2013.)

Hypotheses

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

Assertion

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

Proof of Theorem impbid2

Step	Hyp	Ref	Expression
1		impbid2.2	. . 3 |- (ph -> (ch -> ps))
2		impbid2.1	. . 3 |- (ps -> ch)
3	1, 2	impbid1 194	. 2 |- (ph -> (ch <-> ps))
4	3	bicomd 192	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:  biimt  325  biorf  394  biorfi  396  pm4.72  846  biort  866  bimsc1  904  euan  2261  cgsexg  2891  cgsex2g  2892  cgsex4g  2893  elab3gf  2991  abidnf  3006  elsnc2g  3762  difsn  3846  eqsn  3868  dfnfc2  3910  intmin4  3956  dfiin2g  4001  eqpw1uni  4331  eqfnfv  5393  ffvresb  5432  fnoprabg  5586  ncssfin  6152  ce0lenc1  6240