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  5531  tz6.12c  5670  fnbrfvb  5685  ssimaex  5708  fvimacnv  5763  elpreima  5767  fsn  5820  fconst2g  5870  fndmexb  5878  elunirn  5910  f1ocnvfvb  5924  foeqcnvco  5934  f1eqcocnv  5935  fliftfun  5940  isose  5965  isopo  5967  isoso  5969  f1oiso2  5971  eusvobj2  6007  oprabid  6053  f1opw2  6232  op1steq  6345  rntpos  6426  frecabcl  6568  nnsucelsuc  6662  nnsucsssuc  6663  nnsseleq  6672  nnaord  6680  nnmord  6688  nnaordex  6699  nnawordex  6700  nnm00  6701  erexb  6730  swoord1  6734  swoord2  6735  iinerm  6779  fundmen  6984  dom1o  7005  mapxpen  7037  ssenen  7040  nneneq  7046  nndomo  7053  fidifsnen  7060  en1eqsnbi  7151  suplub2ti  7203  isoti  7209  ordiso2  7237  ordiso  7238  ctm  7311  ctssdc  7315  enomni  7341  enmkv  7364  enwomni  7372  pm54.43  7398  pr2ne  7400  ltexnqq  7631  genprndl  7744  genprndu  7745  nqprl  7774  nqpru  7775  1idprl  7813  1idpru  7814  ltexprlemrnd  7828  ltaprg  7842  recexprlemrnd  7852  cauappcvgprlemrnd  7873  caucvgprlemrnd  7896  caucvgprprlemrnd  7924  suplocexprlemrl  7940  suplocexprlemru  7942  map2psrprg  8028  ltxrlt  8248  lttri3  8262  addlsub  8552  addid0  8555  ltadd2  8602  eqord1  8666  reapti  8762  apreap  8770  ltmul1  8775  apreim  8786  ltleap  8815  mulap0b  8838  recapb  8854  apmul1  8971  rerecapb  9026  lt2msq  9069  nnsub  9185  zltnle  9528  zleloe  9529  zrevaddcl  9533  zltp1le  9537  zapne  9557  nn0n0n1ge2b  9562  zdiv  9571  nneo  9586  zeo2  9589  qrevaddcl  9881  npnflt  10053  nmnfgt  10056  xltneg  10074  xleadd1  10113  iccid  10163  zltaddlt1le  10245  fzn  10280  0fz1  10283  uzsplit  10330  fzm1  10338  fzrevral  10343  ssfzo12bi  10474  qltnle  10507  ioo0  10523  ioom  10524  ico0  10525  ioc0  10526  flqge  10546  modqid2  10617  modqmuladd  10632  frec2uzlt2d  10670  seqf1oglem1  10785  qsqeqor  10916  nn0ltexp2  10975  hashtpg  11115  len0nnbi  11155  ccats1pfxeqbi  11330  reuccatpfxs1  11335  shftlem  11397  shftuz  11398  caucvgrelemcau  11561  sqrtsq  11625  abs00ap  11643  cau3lem  11695  maxleb  11797  rexico  11802  negfi  11809  climshft  11885  zsumdc  11966  fsum3  11969  fsum00  12044  zproddc  12161  fprodseq  12165  dvdsval2  12372  moddvds  12381  negdvdsb  12389  dvdsnegb  12390  dvdscmulr  12402  dvdsmulcr  12403  dvdssub2  12417  fzo0dvdseq  12439  ltoddhalfle  12475  dvdsgcdb  12605  gcdzeq  12614  dvdssqlem  12622  lcmeq0  12664  lcmdvdsb  12677  coprmgcdb  12681  ncoprmgcdne1b  12682  cncongr  12698  isprm2lem  12709  dvdsprime  12715  dvdsprm  12730  coprm  12737  euclemma  12739  rpexp  12746  prmdiveq  12829  hashgcdlem  12831  odzdvds  12839  pythagtrip  12877  pcdvdsb  12914  pc2dvds  12924  pcprmpw2  12927  pcprmpw  12928  enct  13075  intopsn  13471  gsumfzval  13495  isgrpid2  13644  isgrpinv  13658  f1ghm0to0  13880  ringinvnz1ne0  14084  ringinvnzdiv  14085  unitmulclb  14150  dvreq1  14178  isnzr2  14220  rrgeq0  14301  domneq0  14308  lssats2  14450  lspsneq0  14462  znunit  14695  toponcomb  14779  tgss3  14829  isopn3  14876  neiint  14896  neipsm  14905  opnneissb  14906  opnssneib  14907  tpnei  14911  opnneiid  14915  restopnb  14932  tgcn  14959  tgcnp  14960  iscnp4  14969  cnpnei  14970  cnntr  14976  lmss  14997  upxp  15023  txcn  15026  txlm  15030  hmeoopn  15062  hmeocld  15063  xblm  15168  blssexps  15180  blssex  15181  isxms2  15203  neibl  15242  metss  15245  metrest  15257  metcnp3  15262  ivthinclemlr  15388  ivthinclemur  15390  cnplimccntop  15421  eflt  15526  dvdsppwf1o  15740  lgsdir2lem4  15787  lgsne0  15794  gausslemma2dlem1a  15814  lgsquadlem1  15833  m1lgs  15841  uhgr0vb  15962  ausgrusgrben  16046  ushgredgedg  16104  ushgredgedgloop  16106  usgr0vb  16111  loopclwwlkn1b  16297  eupth2lem3lem4fi  16351  bj-charfunbi  16465  subctctexmid  16660  triap  16692  iswomni0  16715