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  702  nbn2  704  2falsed  709  pm5.21ndd  712  oibabs  721  orbi2d  797  con4biddc  864  con1bidc  881  con1bdc  885  dedlema  977  dedlemb  978  xorbin  1428  albi  1516  19.21ht  1629  exbi  1652  19.23t  1725  equequ1  1760  equequ2  1761  equsexd  1777  dral1  1778  cbv2h  1796  cbv2w  1798  sbequ12  1819  sbiedh  1835  drex1  1846  ax11b  1874  sbequ  1888  sbft  1896  sb56  1934  cbvexdh  1975  eupickb  2161  eupickbi  2162  elequ1  2206  elequ2  2207  ceqsalt  2829  ceqex  2933  mob2  2986  euxfr2dc  2991  reu6  2995  sbciegft  3062  csbiebt  3167  sseq1  3250  reupick  3491  reupick2  3493  disjeq2  4068  disjeq1  4071  exmidsssnc  4293  copsexg  4336  euotd  4347  poeq2  4397  sotritric  4421  sotritrieq  4422  seeq1  4436  seeq2  4437  alxfr  4558  ralxfrd  4559  rexxfrd  4560  ordelsuc  4603  sosng  4799  iss  5059  iotaval  5298  funeq  5346  funssres  5369  f0dom0  5530  tz6.12c  5669  fnbrfvb  5684  ssimaex  5707  fvimacnv  5762  elpreima  5766  fsn  5819  fconst2g  5869  elunirn  5907  f1ocnvfvb  5921  foeqcnvco  5931  f1eqcocnv  5932  fliftfun  5937  isose  5962  isopo  5964  isoso  5966  f1oiso2  5968  eusvobj2  6004  oprabid  6050  f1opw2  6229  op1steq  6342  rntpos  6423  frecabcl  6565  nnsucelsuc  6659  nnsucsssuc  6660  nnsseleq  6669  nnaord  6677  nnmord  6685  nnaordex  6696  nnawordex  6697  nnm00  6698  erexb  6727  swoord1  6731  swoord2  6732  iinerm  6776  fundmen  6981  dom1o  7002  mapxpen  7034  ssenen  7037  nneneq  7043  nndomo  7050  fidifsnen  7057  en1eqsnbi  7148  suplub2ti  7200  isoti  7206  ordiso2  7234  ordiso  7235  ctm  7308  ctssdc  7312  enomni  7338  enmkv  7361  enwomni  7369  pm54.43  7395  pr2ne  7397  ltexnqq  7628  genprndl  7741  genprndu  7742  nqprl  7771  nqpru  7772  1idprl  7810  1idpru  7811  ltexprlemrnd  7825  ltaprg  7839  recexprlemrnd  7849  cauappcvgprlemrnd  7870  caucvgprlemrnd  7893  caucvgprprlemrnd  7921  suplocexprlemrl  7937  suplocexprlemru  7939  map2psrprg  8025  ltxrlt  8245  lttri3  8259  addlsub  8549  addid0  8552  ltadd2  8599  eqord1  8663  reapti  8759  apreap  8767  ltmul1  8772  apreim  8783  ltleap  8812  mulap0b  8835  recapb  8851  apmul1  8968  rerecapb  9023  lt2msq  9066  nnsub  9182  zltnle  9525  zleloe  9526  zrevaddcl  9530  zltp1le  9534  zapne  9554  nn0n0n1ge2b  9559  zdiv  9568  nneo  9583  zeo2  9586  qrevaddcl  9878  npnflt  10050  nmnfgt  10053  xltneg  10071  xleadd1  10110  iccid  10160  zltaddlt1le  10242  fzn  10277  0fz1  10280  uzsplit  10327  fzm1  10335  fzrevral  10340  ssfzo12bi  10471  qltnle  10504  ioo0  10520  ioom  10521  ico0  10522  ioc0  10523  flqge  10543  modqid2  10614  modqmuladd  10629  frec2uzlt2d  10667  seqf1oglem1  10782  qsqeqor  10913  nn0ltexp2  10972  len0nnbi  11149  ccats1pfxeqbi  11324  reuccatpfxs1  11329  shftlem  11378  shftuz  11379  caucvgrelemcau  11542  sqrtsq  11606  abs00ap  11624  cau3lem  11676  maxleb  11778  rexico  11783  negfi  11790  climshft  11866  zsumdc  11947  fsum3  11950  fsum00  12025  zproddc  12142  fprodseq  12146  dvdsval2  12353  moddvds  12362  negdvdsb  12370  dvdsnegb  12371  dvdscmulr  12383  dvdsmulcr  12384  dvdssub2  12398  fzo0dvdseq  12420  ltoddhalfle  12456  dvdsgcdb  12586  gcdzeq  12595  dvdssqlem  12603  lcmeq0  12645  lcmdvdsb  12658  coprmgcdb  12662  ncoprmgcdne1b  12663  cncongr  12679  isprm2lem  12690  dvdsprime  12696  dvdsprm  12711  coprm  12718  euclemma  12720  rpexp  12727  prmdiveq  12810  hashgcdlem  12812  odzdvds  12820  pythagtrip  12858  pcdvdsb  12895  pc2dvds  12905  pcprmpw2  12908  pcprmpw  12909  enct  13056  intopsn  13452  gsumfzval  13476  isgrpid2  13625  isgrpinv  13639  f1ghm0to0  13861  ringinvnz1ne0  14065  ringinvnzdiv  14066  unitmulclb  14131  dvreq1  14159  isnzr2  14201  rrgeq0  14282  domneq0  14289  lssats2  14431  lspsneq0  14443  znunit  14676  toponcomb  14755  tgss3  14805  isopn3  14852  neiint  14872  neipsm  14881  opnneissb  14882  opnssneib  14883  tpnei  14887  opnneiid  14891  restopnb  14908  tgcn  14935  tgcnp  14936  iscnp4  14945  cnpnei  14946  cnntr  14952  lmss  14973  upxp  14999  txcn  15002  txlm  15006  hmeoopn  15038  hmeocld  15039  xblm  15144  blssexps  15156  blssex  15157  isxms2  15179  neibl  15218  metss  15221  metrest  15233  metcnp3  15238  ivthinclemlr  15364  ivthinclemur  15366  cnplimccntop  15397  eflt  15502  dvdsppwf1o  15716  lgsdir2lem4  15763  lgsne0  15770  gausslemma2dlem1a  15790  lgsquadlem1  15809  m1lgs  15817  uhgr0vb  15938  ausgrusgrben  16022  ushgredgedg  16080  ushgredgedgloop  16082  usgr0vb  16087  loopclwwlkn1b  16273  eupth2lem3lem4fi  16327  bj-charfunbi  16423  subctctexmid  16618  triap  16650  iswomni0  16672