Theorem impbid2 517

Description: Infer an equivalence from two implications.

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.1	. . 3 |- (ps -> ch)
2	1	a1i 8	. 2 |- (ph -> (ps -> ch))
3		impbid2.2	. 2 |- (ph -> (ch -> ps))
4	2, 3	impbid 515	1 |- (ph -> (ps <-> ch))

Syntax hints:   -> wi 3   <-> wb 146

This theorem is referenced by:  pm4.72 640  mtt 711  biimt 730  biort 733  dedlem0a 759  dedlema 761  19.23t 1114  cgsexg 1827  cgsex2g 1828  cgsex4g 1829  elab3g 1898  abidhb 1908  hbsbc1gd 1979  hbsbcgd 1980  uniiunlem 2128  elsnc2g 2432  eqsn 2470  prel12 2480  intmin4 2554  elpw2g 2722  opelopab2 2814  difex2 2872  ord0eln0 3018  ordpwsuc 3061  ordunisuc2 3110  limsssuc 3116  dfom2 3128  opres 3367  cores 3491  relcnvexb 3513  f1ocnvb 3693  fnoprabg 4003  omord 4189  nneob 4245  pw2en 4432  sbthbg 4444  ltexpq2 5061  nltpnftt 5547  ngtmnftt 5548  xrrebndt 5549  supxrre 6038  elnn0nn 6126  ioonegt 6347  iccnegt 6348  fz1sbct 6457  reim0bt 6720  clm3 7025  bastopt 7583  0top 7585  bastop 7592  subtop 7596  neiint 7669  islp2 7697  hmopadj2t 9804  mdslle1 10181  mdslle2 10182  elghomlem2 10317

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7

This theorem depends on definitions:  df-bi 147  df-an 225

Copyright terms: Public domain