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  2890  cgsex2g  2891  cgsex4g  2892  elab3gf  2990  abidnf  3005  elsnc2g  3761  difsn  3845  eqsn  3867  dfnfc2  3909  intmin4  3955  dfiin2g  4000  eqpw1uni  4330  eqfnfv  5392  ffvresb  5431  fnoprabg  5585  ncssfin  6151  ce0lenc1  6239