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  667  pm5.21  696  nbn2  698  2falsed  703  pm5.21ndd  706  oibabs  715  orbi2d  791  con4biddc  858  con1bidc  875  con1bdc  879  dedlema  971  dedlemb  972  xorbin  1395  albi  1482  19.21ht  1595  exbi  1618  19.23t  1691  equequ1  1726  equequ2  1727  equsexd  1743  dral1  1744  cbv2h  1762  cbv2w  1764  sbequ12  1785  sbiedh  1801  drex1  1812  ax11b  1840  sbequ  1854  sbft  1862  sb56  1900  cbvexdh  1941  eupickb  2126  eupickbi  2127  elequ1  2171  elequ2  2172  ceqsalt  2789  ceqex  2891  mob2  2944  euxfr2dc  2949  reu6  2953  sbciegft  3020  csbiebt  3124  sseq1  3206  reupick  3447  reupick2  3449  disjeq2  4014  disjeq1  4017  exmidsssnc  4236  copsexg  4277  euotd  4287  poeq2  4335  sotritric  4359  sotritrieq  4360  seeq1  4374  seeq2  4375  alxfr  4496  ralxfrd  4497  rexxfrd  4498  ordelsuc  4541  sosng  4736  iss  4992  iotaval  5230  funeq  5278  funssres  5300  f0dom0  5451  tz6.12c  5588  fnbrfvb  5601  ssimaex  5622  fvimacnv  5677  elpreima  5681  fsn  5734  fconst2g  5777  elunirn  5813  f1ocnvfvb  5827  foeqcnvco  5837  f1eqcocnv  5838  fliftfun  5843  isose  5868  isopo  5870  isoso  5872  f1oiso2  5874  eusvobj2  5908  oprabid  5954  f1opw2  6129  op1steq  6237  rntpos  6315  frecabcl  6457  nnsucelsuc  6549  nnsucsssuc  6550  nnsseleq  6559  nnaord  6567  nnmord  6575  nnaordex  6586  nnawordex  6587  nnm00  6588  erexb  6617  swoord1  6621  swoord2  6622  iinerm  6666  fundmen  6865  mapxpen  6909  ssenen  6912  nneneq  6918  nndomo  6925  fidifsnen  6931  en1eqsnbi  7015  suplub2ti  7067  isoti  7073  ordiso2  7101  ordiso  7102  ctm  7175  ctssdc  7179  enomni  7205  enmkv  7228  enwomni  7236  pm54.43  7257  pr2ne  7259  ltexnqq  7475  genprndl  7588  genprndu  7589  nqprl  7618  nqpru  7619  1idprl  7657  1idpru  7658  ltexprlemrnd  7672  ltaprg  7686  recexprlemrnd  7696  cauappcvgprlemrnd  7717  caucvgprlemrnd  7740  caucvgprprlemrnd  7768  suplocexprlemrl  7784  suplocexprlemru  7786  map2psrprg  7872  ltxrlt  8092  lttri3  8106  addlsub  8396  addid0  8399  ltadd2  8446  eqord1  8510  reapti  8606  apreap  8614  ltmul1  8619  apreim  8630  ltleap  8659  mulap0b  8682  recapb  8698  apmul1  8815  rerecapb  8870  lt2msq  8913  nnsub  9029  zltnle  9372  zleloe  9373  zrevaddcl  9376  zltp1le  9380  zapne  9400  nn0n0n1ge2b  9405  zdiv  9414  nneo  9429  zeo2  9432  qrevaddcl  9718  npnflt  9890  nmnfgt  9893  xltneg  9911  xleadd1  9950  iccid  10000  zltaddlt1le  10082  fzn  10117  0fz1  10120  uzsplit  10167  fzm1  10175  fzrevral  10180  ssfzo12bi  10301  qltnle  10333  ioo0  10349  ioom  10350  ico0  10351  ioc0  10352  flqge  10372  modqid2  10443  modqmuladd  10458  frec2uzlt2d  10496  seqf1oglem1  10611  qsqeqor  10742  nn0ltexp2  10801  len0nnbi  10969  shftlem  10981  shftuz  10982  caucvgrelemcau  11145  sqrtsq  11209  abs00ap  11227  cau3lem  11279  maxleb  11381  rexico  11386  negfi  11393  climshft  11469  zsumdc  11549  fsum3  11552  fsum00  11627  zproddc  11744  fprodseq  11748  dvdsval2  11955  moddvds  11964  negdvdsb  11972  dvdsnegb  11973  dvdscmulr  11985  dvdsmulcr  11986  dvdssub2  12000  fzo0dvdseq  12022  ltoddhalfle  12058  dvdsgcdb  12180  gcdzeq  12189  dvdssqlem  12197  lcmeq0  12239  lcmdvdsb  12252  coprmgcdb  12256  ncoprmgcdne1b  12257  cncongr  12273  isprm2lem  12284  dvdsprime  12290  dvdsprm  12305  coprm  12312  euclemma  12314  rpexp  12321  prmdiveq  12404  hashgcdlem  12406  odzdvds  12414  pythagtrip  12452  pcdvdsb  12489  pc2dvds  12499  pcprmpw2  12502  pcprmpw  12503  enct  12650  intopsn  13010  gsumfzval  13034  isgrpid2  13172  isgrpinv  13186  f1ghm0to0  13402  ringinvnz1ne0  13605  ringinvnzdiv  13606  unitmulclb  13670  dvreq1  13698  isnzr2  13740  rrgeq0  13821  domneq0  13828  lssats2  13970  lspsneq0  13982  znunit  14215  toponcomb  14264  tgss3  14314  isopn3  14361  neiint  14381  neipsm  14390  opnneissb  14391  opnssneib  14392  tpnei  14396  opnneiid  14400  restopnb  14417  tgcn  14444  tgcnp  14445  iscnp4  14454  cnpnei  14455  cnntr  14461  lmss  14482  upxp  14508  txcn  14511  txlm  14515  hmeoopn  14547  hmeocld  14548  xblm  14653  blssexps  14665  blssex  14666  isxms2  14688  neibl  14727  metss  14730  metrest  14742  metcnp3  14747  ivthinclemlr  14873  ivthinclemur  14875  cnplimccntop  14906  eflt  15011  dvdsppwf1o  15225  lgsdir2lem4  15272  lgsne0  15279  gausslemma2dlem1a  15299  lgsquadlem1  15318  m1lgs  15326  bj-charfunbi  15457  subctctexmid  15645  triap  15673  iswomni0  15695