Theorem impbid 129

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

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

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

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  bicom1  131  impbid1  142  pm5.74  179  imbi1d  231  pm5.501  244  pm5.32d  450  impbida  600  notbi  672  pm5.21  703  nbn2  705  2falsed  710  pm5.21ndd  713  oibabs  722  orbi2d  798  con4biddc  865  con1bidc  882  con1bdc  886  dedlema  978  dedlemb  979  xorbin  1429  albi  1517  19.21ht  1630  exbi  1653  19.23t  1725  equequ1  1760  equequ2  1761  equsexd  1778  dral1  1779  cbv2h  1797  cbv2w  1799  sbequ12  1820  sbiedh  1836  drex1  1847  ax11b  1875  sbequ  1889  sbft  1897  sb56  1936  cbvexdh  1978  eupickb  2164  eupickbi  2165  elequ1  2209  elequ2  2210  ceqsalt  2842  ceqex  2946  mob2  2999  euxfr2dc  3004  reu6  3008  sbciegft  3075  csbiebt  3180  sseq1  3263  reupick  3507  reupick2  3509  disjeq2  4091  disjeq1  4094  exmidsssnc  4318  copsexg  4362  euotd  4373  poeq2  4423  sotritric  4447  sotritrieq  4448  seeq1  4462  seeq2  4463  alxfr  4584  ralxfrd  4585  rexxfrd  4586  ordelsuc  4629  sosng  4825  iss  5086  iotaval  5326  funeq  5374  funssres  5397  f0dom0  5563  tz6.12c  5702  fnbrfvb  5717  ssimaex  5740  fvimacnv  5795  elpreima  5799  fsn  5851  fconst2g  5901  fndmexb  5909  elunirn  5941  f1ocnvfvb  5955  foeqcnvco  5965  f1eqcocnv  5966  fliftfun  5971  isose  5996  isopo  5998  isoso  6000  f1oiso2  6002  eusvobj2  6038  oprabid  6084  f1opw2  6263  op1steq  6375  fvn0elsuppb  6454  rntpos  6490  frecabcl  6632  nnsucelsuc  6726  nnsucsssuc  6727  nnsseleq  6736  nnaord  6744  nnmord  6752  nnaordex  6763  nnawordex  6764  nnm00  6765  erexb  6794  swoord1  6798  swoord2  6799  iinerm  6843  mapsnd  6925  fundmen  7049  dom1o  7071  mapxpen  7103  mapunen  7106  ssenen  7107  nneneq  7113  nndomo  7120  fidifsnen  7127  en1eqsnbi  7221  suplub2ti  7294  isoti  7300  ordiso2  7328  ordiso  7329  ctm  7402  ctssdc  7406  enomni  7432  enmkv  7455  enwomni  7463  pm54.43  7489  pr2ne  7491  ltexnqq  7725  genprndl  7838  genprndu  7839  nqprl  7868  nqpru  7869  1idprl  7907  1idpru  7908  ltexprlemrnd  7922  ltaprg  7936  recexprlemrnd  7946  cauappcvgprlemrnd  7967  caucvgprlemrnd  7990  caucvgprprlemrnd  8018  suplocexprlemrl  8034  suplocexprlemru  8036  map2psrprg  8122  ltxrlt  8341  lttri3  8355  addlsub  8645  addid0  8648  ltadd2  8695  eqord1  8759  reapti  8855  apreap  8863  ltmul1  8868  apreim  8879  ltleap  8908  mulap0b  8931  recapb  8947  apmul1  9064  rerecapb  9119  lt2msq  9162  nnsub  9278  zltnle  9625  zleloe  9626  zrevaddcl  9630  zltp1le  9634  zapne  9654  nn0n0n1ge2b  9660  zdiv  9669  nneo  9684  zeo2  9687  qrevaddcl  9979  npnflt  10151  nmnfgt  10154  xltneg  10172  xleadd1  10211  iccid  10261  zltaddlt1le  10344  fzn  10379  0fz1  10382  uzsplit  10430  fzm1  10438  fzrevral  10443  ssfzo12bi  10574  qltnle  10607  ioo0  10623  ioom  10624  ico0  10625  ioc0  10626  flqge  10646  modqid2  10717  modqmuladd  10732  frec2uzlt2d  10770  seqf1oglem1  10885  qsqeqor  11016  nn0ltexp2  11075  hashtpg  11223  len0nnbi  11263  ccats1pfxeqbi  11438  reuccatpfxs1  11443  shftlem  11505  shftuz  11506  caucvgrelemcau  11669  sqrtsq  11733  abs00ap  11751  cau3lem  11803  maxleb  11905  rexico  11910  negfi  11917  climshft  11993  zsumdc  12074  fsum3  12077  fsum00  12152  zproddc  12269  fprodseq  12273  dvdsval2  12480  moddvds  12489  negdvdsb  12497  dvdsnegb  12498  dvdscmulr  12510  dvdsmulcr  12511  dvdssub2  12525  fzo0dvdseq  12547  ltoddhalfle  12583  dvdsgcdb  12713  gcdzeq  12722  dvdssqlem  12730  lcmeq0  12772  lcmdvdsb  12785  coprmgcdb  12789  ncoprmgcdne1b  12790  cncongr  12806  isprm2lem  12817  dvdsprime  12823  dvdsprm  12838  coprm  12845  euclemma  12847  rpexp  12854  prmdiveq  12937  hashgcdlem  12939  odzdvds  12947  pythagtrip  12985  pcdvdsb  13022  pc2dvds  13032  pcprmpw2  13035  pcprmpw  13036  enct  13201  intopsn  13597  gsumfzval  13621  isgrpid2  13770  isgrpinv  13784  f1ghm0to0  14006  ringinvnz1ne0  14210  ringinvnzdiv  14211  unitmulclb  14276  dvreq1  14304  isnzr2  14346  rrgeq0  14427  domneq0  14435  lssats2  14579  lspsneq0  14591  znunit  14824  toponcomb  14910  tgss3  14960  isopn3  15007  neiint  15027  neipsm  15036  opnneissb  15037  opnssneib  15038  tpnei  15042  opnneiid  15046  restopnb  15063  tgcn  15090  tgcnp  15091  iscnp4  15100  cnpnei  15101  cnntr  15107  lmss  15128  upxp  15154  txcn  15157  txlm  15161  hmeoopn  15193  hmeocld  15194  xblm  15299  blssexps  15311  blssex  15312  isxms2  15334  neibl  15373  metss  15376  metrest  15388  metcnp3  15393  ivthinclemlr  15519  ivthinclemur  15521  cnplimccntop  15552  eflt  15657  dvdsppwf1o  15874  lgsdir2lem4  15921  lgsne0  15928  gausslemma2dlem1a  15948  lgsquadlem1  15967  m1lgs  15975  uhgr0vb  16096  ausgrusgrben  16180  ushgredgedg  16238  ushgredgedgloop  16240  usgr0vb  16245  loopclwwlkn1b  16431  eupth2lem3lem4fi  16485  bj-charfunbi  16598  subctctexmid  16791  triap  16830  iswomni0  16853