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  596  notbi  666  pm5.21  695  nbn2  697  2falsed  702  pm5.21ndd  705  oibabs  714  orbi2d  790  con4biddc  857  con1bidc  874  con1bdc  878  dedlema  969  dedlemb  970  xorbin  1384  albi  1468  19.21ht  1581  exbi  1604  19.23t  1677  equequ1  1712  equequ2  1713  equsexd  1729  dral1  1730  cbv2h  1748  cbv2w  1750  sbequ12  1771  sbiedh  1787  drex1  1798  ax11b  1826  sbequ  1840  sbft  1848  sb56  1885  cbvexdh  1926  eupickb  2107  eupickbi  2108  elequ1  2152  elequ2  2153  ceqsalt  2764  ceqex  2865  mob2  2918  euxfr2dc  2923  reu6  2927  sbciegft  2994  csbiebt  3097  sseq1  3179  reupick  3420  reupick2  3422  disjeq2  3985  disjeq1  3988  exmidsssnc  4204  copsexg  4245  euotd  4255  poeq2  4301  sotritric  4325  sotritrieq  4326  seeq1  4340  seeq2  4341  alxfr  4462  ralxfrd  4463  rexxfrd  4464  ordelsuc  4505  sosng  4700  iss  4954  iotaval  5190  funeq  5237  funssres  5259  f0dom0  5410  tz6.12c  5546  fnbrfvb  5557  ssimaex  5578  fvimacnv  5632  elpreima  5636  fsn  5689  fconst2g  5732  elunirn  5767  f1ocnvfvb  5781  foeqcnvco  5791  f1eqcocnv  5792  fliftfun  5797  isose  5822  isopo  5824  isoso  5826  f1oiso2  5828  eusvobj2  5861  oprabid  5907  f1opw2  6077  op1steq  6180  rntpos  6258  frecabcl  6400  nnsucelsuc  6492  nnsucsssuc  6493  nnsseleq  6502  nnaord  6510  nnmord  6518  nnaordex  6529  nnawordex  6530  nnm00  6531  erexb  6560  swoord1  6564  swoord2  6565  iinerm  6607  fundmen  6806  mapxpen  6848  ssenen  6851  nneneq  6857  nndomo  6864  fidifsnen  6870  en1eqsnbi  6948  suplub2ti  7000  isoti  7006  ordiso2  7034  ordiso  7035  ctm  7108  ctssdc  7112  enomni  7137  enmkv  7160  enwomni  7168  pm54.43  7189  pr2ne  7191  ltexnqq  7407  genprndl  7520  genprndu  7521  nqprl  7550  nqpru  7551  1idprl  7589  1idpru  7590  ltexprlemrnd  7604  ltaprg  7618  recexprlemrnd  7628  cauappcvgprlemrnd  7649  caucvgprlemrnd  7672  caucvgprprlemrnd  7700  suplocexprlemrl  7716  suplocexprlemru  7718  map2psrprg  7804  ltxrlt  8023  lttri3  8037  addlsub  8327  addid0  8330  ltadd2  8376  eqord1  8440  reapti  8536  apreap  8544  ltmul1  8549  apreim  8560  ltleap  8589  mulap0b  8612  recapb  8628  apmul1  8745  rerecapb  8800  lt2msq  8843  nnsub  8958  zltnle  9299  zleloe  9300  zrevaddcl  9303  zltp1le  9307  zapne  9327  nn0n0n1ge2b  9332  zdiv  9341  nneo  9356  zeo2  9359  qrevaddcl  9644  npnflt  9815  nmnfgt  9818  xltneg  9836  xleadd1  9875  iccid  9925  zltaddlt1le  10007  fzn  10042  0fz1  10045  uzsplit  10092  fzm1  10100  fzrevral  10105  ssfzo12bi  10225  qltnle  10246  ioo0  10260  ioom  10261  ico0  10262  ioc0  10263  flqge  10282  modqid2  10351  modqmuladd  10366  frec2uzlt2d  10404  qsqeqor  10631  nn0ltexp2  10689  shftlem  10825  shftuz  10826  caucvgrelemcau  10989  sqrtsq  11053  abs00ap  11071  cau3lem  11123  maxleb  11225  rexico  11230  negfi  11236  climshft  11312  zsumdc  11392  fsum3  11395  fsum00  11470  zproddc  11587  fprodseq  11591  dvdsval2  11797  moddvds  11806  negdvdsb  11814  dvdsnegb  11815  dvdscmulr  11827  dvdsmulcr  11828  dvdssub2  11842  fzo0dvdseq  11863  ltoddhalfle  11898  dvdsgcdb  12014  gcdzeq  12023  dvdssqlem  12031  lcmeq0  12071  lcmdvdsb  12084  coprmgcdb  12088  ncoprmgcdne1b  12089  cncongr  12105  isprm2lem  12116  dvdsprime  12122  dvdsprm  12137  coprm  12144  euclemma  12146  rpexp  12153  prmdiveq  12236  hashgcdlem  12238  odzdvds  12245  pythagtrip  12283  pcdvdsb  12319  pc2dvds  12329  pcprmpw2  12332  pcprmpw  12333  enct  12434  intopsn  12786  isgrpid2  12913  isgrpinv  12926  ringinvnz1ne0  13226  ringinvnzdiv  13227  unitmulclb  13283  dvreq1  13311  toponcomb  13531  tgss3  13581  isopn3  13628  neiint  13648  neipsm  13657  opnneissb  13658  opnssneib  13659  tpnei  13663  opnneiid  13667  restopnb  13684  tgcn  13711  tgcnp  13712  iscnp4  13721  cnpnei  13722  cnntr  13728  lmss  13749  upxp  13775  txcn  13778  txlm  13782  hmeoopn  13814  hmeocld  13815  xblm  13920  blssexps  13932  blssex  13933  isxms2  13955  neibl  13994  metss  13997  metrest  14009  metcnp3  14014  ivthinclemlr  14118  ivthinclemur  14120  cnplimccntop  14142  eflt  14199  lgsdir2lem4  14435  lgsne0  14442  m1lgs  14455  bj-charfunbi  14566  subctctexmid  14753  triap  14780  iswomni0  14802