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 ) )

This proof depends on syntax axioms:   -> wi 4   <-> wb 105

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia2 107  ax-ia3 108

This proof depends on definitions:  df-bi 117

This theorem is used by:  bicom1  131  impbid1  142  pm5.74  179  imbi1d  231  pm5.501  244  pm5.32d  454  impbida  604  notbi  676  pm5.21  707  nbn2  709  2falsed  714  pm5.21ndd  717  oibabs  726  orbi2d  802  con4biddc  869  con1bidc  886  con1bdc  890  dedlema  982  dedlemb  983  xorbin  1433  albi  1521  19.21ht  1634  exbi  1657  19.23t  1729  equequ1  1764  equequ2  1765  equsexd  1782  dral1  1783  cbv2h  1801  cbv2w  1803  sbequ12  1824  sbiedh  1840  drex1  1851  ax11b  1879  sbequ  1893  sbft  1901  sb56  1940  cbvexdh  1982  eupickb  2168  eupickbi  2169  elequ1  2213  elequ2  2214  ceqsalt  2848  ceqex  2953  mob2  3006  euxfr2dc  3011  reu6  3015  sbciegft  3082  csbiebt  3187  sseq1  3271  reupick  3517  reupick2  3519  disjeq2  4110  disjeq1  4113  exmidsssnc  4340  copsexg  4384  euotd  4395  poeq2  4445  sotritric  4469  sotritrieq  4470  seeq1  4484  seeq2  4485  alxfr  4607  ralxfrd  4608  rexxfrd  4609  ordelsuc  4652  sosng  4848  iss  5109  iotaval  5349  funeq  5397  funssres  5420  f0dom0  5586  tz6.12c  5725  fnbrfvb  5741  ssimaex  5764  fvimacnv  5824  elpreima  5828  fsn  5880  fconst2g  5930  fndmexb  5938  elunirn  5972  f1ocnvfvb  5986  foeqcnvco  5996  f1eqcocnv  5997  fliftfun  6002  isose  6027  isopo  6029  isoso  6031  f1oiso2  6033  eusvobj2  6071  oprabid  6117  f1opw2  6296  op1steq  6413  fvn0elsuppb  6492  rntpos  6528  frecabcl  6670  nnsucelsuc  6764  nnsucsssuc  6765  nnsseleq  6774  nnaord  6782  nnmord  6790  nnaordex  6801  nnawordex  6802  nnm00  6803  erexb  6832  swoord1  6836  swoord2  6837  iinerm  6881  mapsnd  6970  fundmen  7094  dom1o  7116  mapxpen  7148  mapunen  7151  ssenen  7152  nneneq  7158  nndomo  7165  fidifsnen  7172  en1eqsnbi  7266  suplub2ti  7341  isoti  7347  ordiso2  7375  ordiso  7376  ctm  7449  ctssdc  7453  enomni  7479  enmkv  7502  enwomni  7510  pm54.43  7536  pr2ne  7538  ltexnqq  7775  genprndl  7888  genprndu  7889  nqprl  7918  nqpru  7919  1idprl  7957  1idpru  7958  ltexprlemrnd  7972  ltaprg  7986  recexprlemrnd  7996  cauappcvgprlemrnd  8017  caucvgprlemrnd  8040  caucvgprprlemrnd  8068  suplocexprlemrl  8084  suplocexprlemru  8086  map2psrprg  8172  ltxrlt  8391  lttri3  8405  addlsub  8696  addid0  8699  ltadd2  8747  eqord1  8811  reapti  8908  apreap  8916  ltmul1  8921  apreim  8932  ltleap  8961  mulap0b  8984  recapb  9002  apmul1  9119  rerecapb  9174  lt2msq  9217  nnsub  9344  zltnle  9692  zleloe  9693  zrevaddcl  9697  zltp1le  9701  zapne  9721  nn0n0n1ge2b  9727  zdiv  9736  nneo  9751  zeo2  9754  qrevaddcl  10046  npnflt  10219  nmnfgt  10222  xltneg  10240  xleadd1  10279  iccid  10329  zltaddlt1le  10412  fzn  10448  0fz1  10451  uzsplit  10501  fzm1  10509  fzrevral  10514  ssfzo12bi  10645  qltnle  10680  ioo0  10696  ioom  10697  ico0  10698  ioc0  10699  flqge  10719  modqid2  10790  modqmuladd  10805  frec2uzlt2d  10843  seqf1oglem1  10958  qsqeqor  11089  nn0ltexp2  11149  hashtpg  11301  len0nnbi  11341  ccats1pfxeqbi  11516  reuccatpfxs1  11521  shftlem  11583  shftuz  11584  caucvgrelemcau  11748  sqrtsq  11812  abs00ap  11830  cau3lem  11882  maxleb  11984  rexico  11989  negfi  11996  climshft  12072  zsumdc  12153  fsum3  12156  fsum00  12231  zproddc  12348  fprodseq  12352  dvdsval2  12559  moddvds  12568  negdvdsb  12576  dvdsnegb  12577  dvdscmulr  12589  dvdsmulcr  12590  dvdssub2  12604  fzo0dvdseq  12626  ltoddhalfle  12662  dvdsgcdb  12792  gcdzeq  12801  dvdssqlem  12809  lcmeq0  12851  lcmdvdsb  12864  coprmgcdb  12868  ncoprmgcdne1b  12869  cncongr  12885  isprm2lem  12896  dvdsprime  12902  dvdsprm  12917  coprm  12924  euclemma  12926  rpexp  12933  prmdiveq  13016  hashgcdlem  13018  odzdvds  13026  pythagtrip  13064  pcdvdsb  13101  pc2dvds  13111  pcprmpw2  13114  pcprmpw  13115  enct  13326  intopsn  13689  gzsumfzval  13713  isgrpid2  13847  isgrpinv  13861  f1ghm0to0  14077  ringinvnz1ne0  14356  ringinvnzdiv  14357  unitmulclb  14423  dvreq1  14451  isnzr2  14493  rrgeq0  14575  domneq0  14583  lssats2  14753  lspsneq0  14765  znunit  14996  toponcomb  15131  tgss3  15181  isopn3  15228  neiint  15248  neipsm  15257  opnneissb  15258  opnssneib  15259  tpnei  15263  opnneiid  15267  restopnb  15284  tgcn  15311  tgcnp  15312  iscnp4  15321  cnpnei  15322  cnntr  15328  lmss  15349  upxp  15375  txcn  15378  txlm  15382  hmeoopn  15414  hmeocld  15415  xblm  15520  blssexps  15532  blssex  15533  isxms2  15555  neibl  15594  metss  15597  metrest  15609  metcnp3  15614  ivthinclemlr  15740  ivthinclemur  15742  cnplimccntop  15773  eflt  15878  logdivlt  15999  dvdsppwf1o  16109  lgsdir2lem4  16162  lgsne0  16169  gausslemma2dlem1a  16189  lgsquadlem1  16208  m1lgs  16216  uhgr0vb  16337  ausgrusgrben  16421  ushgredgedg  16479  ushgredgedgloop  16481  usgr0vb  16486  loopclwwlkn1b  16672  eupth2lem3lem4fi  16726  lealltlt1  16763  lealltlt2  16764  bj-charfunbi  16849  subctctexmid  17042  stnot  17051  triap  17090  iswomni0  17113  alsralrex  17165