Theorem impbid 183

Description: Deduce an equivalence from two implications. (Contributed by NM, 5-Aug-1993.) (Revised by Wolf Lammen, 3-Nov-2012.)

Hypotheses

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

Assertion

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

Proof of Theorem impbid

Step	Hyp	Ref	Expression
1		impbid.1	. . 3 |- (ph -> (ps -> ch))
2		impbid.2	. . 3 |- (ph -> (ch -> ps))
3	1, 2	impbid21d 182	. 2 |- (ph -> (ph -> (ps <-> ch)))
4	3	pm2.43i 43	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:  bicom1  190  impbid1  194  impcon4bid  196  pm5.74  235  imbi1d  308  pm5.501  330  2falsed  340  impbida  805  dedlem0b  919  dedlema  920  dedlemb  921  albi  1564  exbi  1581  equequ1  1684  equequ1OLD  1685  elequ1  1713  elequ2  1715  19.21t  1795  19.23t  1800  19.23tOLD  1819  19.21tOLD  1863  sbequ12  1919  dral1  1965  cbv2h  1980  ax11b  1995  sbft  2025  sbied  2036  sbequ  2060  sb56  2098  sbal1  2126  exsb  2130  dral1-o  2154  eupickb  2269  eupickbi  2270  2eu2  2285  ceqsalt  2882  ceqex  2970  mob2  3017  reu6  3026  sbciegft  3077  eqsbc2  3104  csbiebt  3173  sseq1  3293  reupick  3540  reupick2  3542  uneqdifeq  3639  iotaval  4351  lenltfin  4470  ncfineleq  4478  tfinltfin  4502  copsexg  4608  iss  5001  funssres  5145  tz6.12c  5348  fvimacnv  5404  elpreima  5408  fsn  5433  fconst2g  5453  fconst5  5456  f1ocnvfvb  5480  f1oiso2  5501  oprabid  5551  erth  5969  enprmaplem5  6081  ncdisjun  6137  ce0addcnnul  6180  ce0nnulb  6183  ceclb  6184  ltlenlec  6208  dflec2  6211  tlecg  6231  muc0or  6253  lecadd2  6267  ncslesuc  6268  nchoicelem8  6297