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  4342  copsexg  4386  euotd  4397  poeq2  4447  sotritric  4471  sotritrieq  4472  seeq1  4486  seeq2  4487  alxfr  4609  ralxfrd  4610  rexxfrd  4611  ordelsuc  4654  sosng  4850  iss  5112  iotaval  5352  funeq  5400  funssres  5423  f0dom0  5589  tz6.12c  5728  fnbrfvb  5744  ssimaex  5767  fvimacnv  5827  elpreima  5831  fsn  5883  fconst2g  5933  fndmexb  5941  elunirn  5975  f1ocnvfvb  5989  foeqcnvco  5999  f1eqcocnv  6000  fliftfun  6005  isose  6030  isopo  6032  isoso  6034  f1oiso2  6036  eusvobj2  6074  oprabid  6120  f1opw2  6299  op1steq  6417  fvn0elsuppb  6496  rntpos  6532  frecabcl  6674  nnsucelsuc  6768  nnsucsssuc  6769  nnsseleq  6778  nnaord  6786  nnmord  6794  nnaordex  6805  nnawordex  6806  nnm00  6807  erexb  6836  swoord1  6840  swoord2  6841  iinerm  6885  mapsnd  6975  fundmen  7099  dom1o  7121  mapxpen  7153  mapunen  7156  ssenen  7157  nneneq  7163  nndomo  7170  fidifsnen  7177  en1eqsnbi  7272  suplub2ti  7348  isoti  7354  ordiso2  7382  ordiso  7383  ctm  7456  ctssdc  7460  enomni  7486  enmkv  7509  enwomni  7517  pm54.43  7543  pr2ne  7545  ltexnqq  7782  genprndl  7895  genprndu  7896  nqprl  7925  nqpru  7926  1idprl  7964  1idpru  7965  ltexprlemrnd  7979  ltaprg  7993  recexprlemrnd  8003  cauappcvgprlemrnd  8024  caucvgprlemrnd  8047  caucvgprprlemrnd  8075  suplocexprlemrl  8091  suplocexprlemru  8093  map2psrprg  8179  ltxrlt  8398  lttri3  8412  addlsub  8704  addid0  8707  ltadd2  8755  eqord1  8819  reapti  8916  apreap  8924  ltmul1  8929  apreim  8940  ltleap  8969  mulap0b  8992  recapb  9010  apmul1  9127  rerecapb  9182  lt2msq  9225  nnsub  9353  zltnle  9702  zleloe  9703  zrevaddcl  9707  zltp1le  9711  zapne  9731  nn0n0n1ge2b  9737  zdiv  9746  nneo  9761  zeo2  9764  qrevaddcl  10061  npnflt  10235  nmnfgt  10238  xltneg  10256  xleadd1  10295  iccid  10345  zltaddlt1le  10428  fzn  10464  0fz1  10467  uzsplit  10517  fzm1  10525  fzrevral  10530  ssfzo12bi  10661  qltnle  10696  ioo0  10712  ioom  10713  ico0  10714  ioc0  10715  flqge  10737  flapge  10738  modqid2  10810  modqmuladd  10825  frec2uzlt2d  10863  seqf1oglem1  10978  qsqeqor  11109  nn0ltexp2  11170  hashtpg  11322  len0nnbi  11362  ccats1pfxeqbi  11537  reuccatpfxs1  11542  shftlem  11604  shftuz  11605  caucvgrelemcau  11769  sqrtsq  11833  abs00ap  11851  cau3lem  11904  maxleb  12006  rexico  12011  negfi  12018  climshft  12096  zsumdc  12177  fsum3  12180  fsum00  12255  zproddc  12372  fprodseq  12376  dvdsval2  12583  moddvds  12592  negdvdsb  12600  dvdsnegb  12601  dvdscmulr  12613  dvdsmulcr  12614  dvdssub2  12628  fzo0dvdseq  12650  ltoddhalfle  12686  dvdsgcdb  12816  gcdzeq  12825  dvdssqlem  12833  lcmeq0  12875  lcmdvdsb  12888  coprmgcdb  12892  ncoprmgcdne1b  12893  cncongr  12909  isprm2lem  12920  dvdsprime  12926  dvdsprm  12942  coprm  12949  euclemma  12951  rpexp  12958  prmdiveq  13044  hashgcdlem  13046  odzdvds  13054  pythagtrip  13092  pcdvdsb  13129  pc2dvds  13139  pcprmpw2  13142  pcprmpw  13143  enct  13383  intopsn  13747  gzsumfzval  13771  isgrpid2  13905  isgrpinv  13919  f1ghm0to0  14135  ringinvnz1ne0  14462  ringinvnzdiv  14463  unitmulclb  14531  dvreq1  14559  isnzr2  14601  rrgeq0  14683  domneq0  14691  lssats2  14861  lspsneq0  14873  znunit  15104  toponcomb  15266  tgss3  15316  isopn3  15363  neiint  15383  neipsm  15392  opnneissb  15393  opnssneib  15394  tpnei  15398  opnneiid  15402  restopnb  15419  tgcn  15446  tgcnp  15447  iscnp4  15456  cnpnei  15457  cnntr  15463  lmss  15484  upxp  15510  txcn  15513  txlm  15517  hmeoopn  15549  hmeocld  15550  xblm  15655  blssexps  15667  blssex  15668  isxms2  15690  neibl  15729  metss  15732  metrest  15744  metcnp3  15749  ivthinclemlr  15875  ivthinclemur  15877  cnplimccntop  15908  eflt  16013  logdivlt  16136  ppiqeq0  16292  dvdsppwf1o  16295  lgsdir2lem4  16367  lgsne0  16374  gausslemma2dlem1a  16394  lgsquadlem1  16413  m1lgs  16421  uhgr0vb  16542  ausgrusgrben  16626  ushgredgedg  16684  ushgredgedgloop  16686  usgr0vb  16691  loopclwwlkn1b  16877  eupth2lem3lem4fi  16931  lealltlt1  16968  lealltlt2  16969  bj-charfunbi  17054  subctctexmid  17247  stnot  17256  triap  17296  iswomni0  17320  alsralrex  17372