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  598  notbi  670  pm5.21  700  nbn2  702  2falsed  707  pm5.21ndd  710  oibabs  719  orbi2d  795  con4biddc  862  con1bidc  879  con1bdc  883  dedlema  975  dedlemb  976  xorbin  1426  albi  1514  19.21ht  1627  exbi  1650  19.23t  1723  equequ1  1758  equequ2  1759  equsexd  1775  dral1  1776  cbv2h  1794  cbv2w  1796  sbequ12  1817  sbiedh  1833  drex1  1844  ax11b  1872  sbequ  1886  sbft  1894  sb56  1932  cbvexdh  1973  eupickb  2159  eupickbi  2160  elequ1  2204  elequ2  2205  ceqsalt  2827  ceqex  2931  mob2  2984  euxfr2dc  2989  reu6  2993  sbciegft  3060  csbiebt  3165  sseq1  3248  reupick  3489  reupick2  3491  disjeq2  4066  disjeq1  4069  exmidsssnc  4291  copsexg  4334  euotd  4345  poeq2  4395  sotritric  4419  sotritrieq  4420  seeq1  4434  seeq2  4435  alxfr  4556  ralxfrd  4557  rexxfrd  4558  ordelsuc  4601  sosng  4797  iss  5057  iotaval  5296  funeq  5344  funssres  5366  f0dom0  5527  tz6.12c  5665  fnbrfvb  5680  ssimaex  5703  fvimacnv  5758  elpreima  5762  fsn  5815  fconst2g  5864  elunirn  5902  f1ocnvfvb  5916  foeqcnvco  5926  f1eqcocnv  5927  fliftfun  5932  isose  5957  isopo  5959  isoso  5961  f1oiso2  5963  eusvobj2  5999  oprabid  6045  f1opw2  6224  op1steq  6337  rntpos  6418  frecabcl  6560  nnsucelsuc  6654  nnsucsssuc  6655  nnsseleq  6664  nnaord  6672  nnmord  6680  nnaordex  6691  nnawordex  6692  nnm00  6693  erexb  6722  swoord1  6726  swoord2  6727  iinerm  6771  fundmen  6976  dom1o  6997  mapxpen  7029  ssenen  7032  nneneq  7038  nndomo  7045  fidifsnen  7052  en1eqsnbi  7142  suplub2ti  7194  isoti  7200  ordiso2  7228  ordiso  7229  ctm  7302  ctssdc  7306  enomni  7332  enmkv  7355  enwomni  7363  pm54.43  7389  pr2ne  7391  ltexnqq  7621  genprndl  7734  genprndu  7735  nqprl  7764  nqpru  7765  1idprl  7803  1idpru  7804  ltexprlemrnd  7818  ltaprg  7832  recexprlemrnd  7842  cauappcvgprlemrnd  7863  caucvgprlemrnd  7886  caucvgprprlemrnd  7914  suplocexprlemrl  7930  suplocexprlemru  7932  map2psrprg  8018  ltxrlt  8238  lttri3  8252  addlsub  8542  addid0  8545  ltadd2  8592  eqord1  8656  reapti  8752  apreap  8760  ltmul1  8765  apreim  8776  ltleap  8805  mulap0b  8828  recapb  8844  apmul1  8961  rerecapb  9016  lt2msq  9059  nnsub  9175  zltnle  9518  zleloe  9519  zrevaddcl  9523  zltp1le  9527  zapne  9547  nn0n0n1ge2b  9552  zdiv  9561  nneo  9576  zeo2  9579  qrevaddcl  9871  npnflt  10043  nmnfgt  10046  xltneg  10064  xleadd1  10103  iccid  10153  zltaddlt1le  10235  fzn  10270  0fz1  10273  uzsplit  10320  fzm1  10328  fzrevral  10333  ssfzo12bi  10463  qltnle  10496  ioo0  10512  ioom  10513  ico0  10514  ioc0  10515  flqge  10535  modqid2  10606  modqmuladd  10621  frec2uzlt2d  10659  seqf1oglem1  10774  qsqeqor  10905  nn0ltexp2  10964  len0nnbi  11141  ccats1pfxeqbi  11316  reuccatpfxs1  11321  shftlem  11370  shftuz  11371  caucvgrelemcau  11534  sqrtsq  11598  abs00ap  11616  cau3lem  11668  maxleb  11770  rexico  11775  negfi  11782  climshft  11858  zsumdc  11938  fsum3  11941  fsum00  12016  zproddc  12133  fprodseq  12137  dvdsval2  12344  moddvds  12353  negdvdsb  12361  dvdsnegb  12362  dvdscmulr  12374  dvdsmulcr  12375  dvdssub2  12389  fzo0dvdseq  12411  ltoddhalfle  12447  dvdsgcdb  12577  gcdzeq  12586  dvdssqlem  12594  lcmeq0  12636  lcmdvdsb  12649  coprmgcdb  12653  ncoprmgcdne1b  12654  cncongr  12670  isprm2lem  12681  dvdsprime  12687  dvdsprm  12702  coprm  12709  euclemma  12711  rpexp  12718  prmdiveq  12801  hashgcdlem  12803  odzdvds  12811  pythagtrip  12849  pcdvdsb  12886  pc2dvds  12896  pcprmpw2  12899  pcprmpw  12900  enct  13047  intopsn  13443  gsumfzval  13467  isgrpid2  13616  isgrpinv  13630  f1ghm0to0  13852  ringinvnz1ne0  14055  ringinvnzdiv  14056  unitmulclb  14121  dvreq1  14149  isnzr2  14191  rrgeq0  14272  domneq0  14279  lssats2  14421  lspsneq0  14433  znunit  14666  toponcomb  14745  tgss3  14795  isopn3  14842  neiint  14862  neipsm  14871  opnneissb  14872  opnssneib  14873  tpnei  14877  opnneiid  14881  restopnb  14898  tgcn  14925  tgcnp  14926  iscnp4  14935  cnpnei  14936  cnntr  14942  lmss  14963  upxp  14989  txcn  14992  txlm  14996  hmeoopn  15028  hmeocld  15029  xblm  15134  blssexps  15146  blssex  15147  isxms2  15169  neibl  15208  metss  15211  metrest  15223  metcnp3  15228  ivthinclemlr  15354  ivthinclemur  15356  cnplimccntop  15387  eflt  15492  dvdsppwf1o  15706  lgsdir2lem4  15753  lgsne0  15760  gausslemma2dlem1a  15780  lgsquadlem1  15799  m1lgs  15807  uhgr0vb  15928  ausgrusgrben  16012  ushgredgedg  16070  ushgredgedgloop  16072  usgr0vb  16077  loopclwwlkn1b  16228  bj-charfunbi  16356  subctctexmid  16551  triap  16583  iswomni0  16605