Theorem impbid 127

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 126	. 2 |- ( ph -> ( ph -> ( ps <-> ch ) ) )
4	3	pm2.43i 48	1 |- ( ph -> ( ps <-> ch ) )

Syntax hints:   -> wi 4   <-> wb 103

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia2 105  ax-ia3 106

This theorem depends on definitions:  df-bi 115

This theorem is referenced by:  bicom1  129  impbid1  140  pm5.74  177  imbi1d  229  pm5.501  242  pm5.32d  438  impbida  563  notbid  627  pm5.21  646  nbn2  648  2falsed  653  pm5.21ndd  656  orbi2d  739  con4biddc  792  con1bidc  806  con1bdc  810  oibabs  838  dedlema  915  dedlemb  916  xorbin  1320  albi  1402  19.21ht  1518  exbi  1540  19.23t  1612  equequ1  1645  equequ2  1646  elequ1  1647  elequ2  1648  equsexd  1664  dral1  1665  cbv2h  1681  sbequ12  1701  sbiedh  1717  drex1  1726  ax11b  1754  sbequ  1768  sbft  1776  sb56  1813  cbvexdh  1849  eupickb  2029  eupickbi  2030  ceqsalt  2645  ceqex  2742  mob2  2793  euxfr2dc  2798  reu6  2802  sbciegft  2867  csbiebt  2965  sseq1  3045  reupick  3281  reupick2  3283  disjeq2  3818  disjeq1  3821  copsexg  4062  euotd  4072  poeq2  4118  sotritric  4142  sotritrieq  4143  seeq1  4157  seeq2  4158  alxfr  4274  ralxfrd  4275  rexxfrd  4276  ordelsuc  4312  sosng  4499  iss  4745  iotaval  4978  funeq  5021  funssres  5042  f0dom0  5188  tz6.12c  5318  fnbrfvb  5329  ssimaex  5349  fvimacnv  5398  elpreima  5402  fsn  5453  fconst2g  5494  elunirn  5527  f1ocnvfvb  5541  foeqcnvco  5551  f1eqcocnv  5552  fliftfun  5557  isose  5582  isopo  5584  isoso  5586  f1oiso2  5588  eusvobj2  5620  oprabid  5663  f1opw2  5832  op1steq  5931  rntpos  6004  frecabcl  6146  nnsucelsuc  6234  nnsucsssuc  6235  nnsseleq  6244  nnaord  6248  nnmord  6256  nnaordex  6266  nnawordex  6267  nnm00  6268  erexb  6297  swoord1  6301  swoord2  6302  iinerm  6344  fundmen  6503  mapxpen  6544  ssenen  6547  nneneq  6553  nndomo  6560  fidifsnen  6566  en1eqsnbi  6637  suplub2ti  6675  isoti  6681  ordiso2  6707  ordiso  6708  enomni  6774  pm54.43  6797  pr2ne  6799  ltexnqq  6946  genprndl  7059  genprndu  7060  nqprl  7089  nqpru  7090  1idprl  7128  1idpru  7129  ltexprlemrnd  7143  ltaprg  7157  recexprlemrnd  7167  cauappcvgprlemrnd  7188  caucvgprlemrnd  7211  caucvgprprlemrnd  7239  ltxrlt  7531  lttri3  7544  addlsub  7827  addid0  7830  ltadd2  7876  reapti  8032  apreap  8040  ltmul1  8045  apreim  8056  ltleap  8083  mulap0b  8098  apmul1  8229  lt2msq  8319  nnsub  8432  zltnle  8766  zleloe  8767  zrevaddcl  8770  zltp1le  8774  zapne  8791  nn0n0n1ge2b  8796  zdiv  8804  nneo  8819  zeo2  8822  qrevaddcl  9098  xltneg  9267  iccid  9312  zltaddlt1le  9392  fzn  9425  0fz1  9428  uzsplit  9473  fzm1  9481  fzrevral  9486  ssfzo12bi  9601  qltnle  9622  ioo0  9636  ioom  9637  ico0  9638  ioc0  9639  flqge  9654  modqid2  9723  modqmuladd  9738  frec2uzlt2d  9776  shftlem  10215  shftuz  10216  caucvgrelemcau  10378  sqrtsq  10442  abs00ap  10460  cau3lem  10512  maxleb  10614  rexico  10619  negfi  10623  climshft  10656  zisum  10738  fisum  10742  fsum00  10819  dvdsval2  10881  moddvds  10887  negdvdsb  10894  dvdsnegb  10895  dvdscmulr  10907  dvdsmulcr  10908  dvdssub2  10920  fzo0dvdseq  10940  ltoddhalfle  10975  dvdsgcdb  11084  gcdzeq  11093  dvdssqlem  11101  lcmeq0  11135  lcmdvdsb  11148  coprmgcdb  11152  ncoprmgcdne1b  11153  cncongr  11169  isprm2lem  11180  dvdsprime  11186  dvdsprm  11200  coprm  11205  euclemma  11207  rpexp  11214  hashgcdlem  11285  bj-notbi  11462