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  1479  19.21ht  1592  exbi  1615  19.23t  1688  equequ1  1723  equequ2  1724  equsexd  1740  dral1  1741  cbv2h  1759  cbv2w  1761  sbequ12  1782  sbiedh  1798  drex1  1809  ax11b  1837  sbequ  1851  sbft  1859  sb56  1897  cbvexdh  1938  eupickb  2119  eupickbi  2120  elequ1  2164  elequ2  2165  ceqsalt  2778  ceqex  2879  mob2  2932  euxfr2dc  2937  reu6  2941  sbciegft  3008  csbiebt  3111  sseq1  3193  reupick  3434  reupick2  3436  disjeq2  4002  disjeq1  4005  exmidsssnc  4224  copsexg  4265  euotd  4275  poeq2  4321  sotritric  4345  sotritrieq  4346  seeq1  4360  seeq2  4361  alxfr  4482  ralxfrd  4483  rexxfrd  4484  ordelsuc  4525  sosng  4720  iss  4974  iotaval  5210  funeq  5258  funssres  5280  f0dom0  5431  tz6.12c  5567  fnbrfvb  5580  ssimaex  5601  fvimacnv  5655  elpreima  5659  fsn  5712  fconst2g  5755  elunirn  5791  f1ocnvfvb  5805  foeqcnvco  5815  f1eqcocnv  5816  fliftfun  5821  isose  5846  isopo  5848  isoso  5850  f1oiso2  5852  eusvobj2  5886  oprabid  5932  f1opw2  6104  op1steq  6208  rntpos  6286  frecabcl  6428  nnsucelsuc  6520  nnsucsssuc  6521  nnsseleq  6530  nnaord  6538  nnmord  6546  nnaordex  6557  nnawordex  6558  nnm00  6559  erexb  6588  swoord1  6592  swoord2  6593  iinerm  6637  fundmen  6836  mapxpen  6880  ssenen  6883  nneneq  6889  nndomo  6896  fidifsnen  6902  en1eqsnbi  6982  suplub2ti  7034  isoti  7040  ordiso2  7068  ordiso  7069  ctm  7142  ctssdc  7146  enomni  7172  enmkv  7195  enwomni  7203  pm54.43  7224  pr2ne  7226  ltexnqq  7442  genprndl  7555  genprndu  7556  nqprl  7585  nqpru  7586  1idprl  7624  1idpru  7625  ltexprlemrnd  7639  ltaprg  7653  recexprlemrnd  7663  cauappcvgprlemrnd  7684  caucvgprlemrnd  7707  caucvgprprlemrnd  7735  suplocexprlemrl  7751  suplocexprlemru  7753  map2psrprg  7839  ltxrlt  8058  lttri3  8072  addlsub  8362  addid0  8365  ltadd2  8411  eqord1  8475  reapti  8571  apreap  8579  ltmul1  8584  apreim  8595  ltleap  8624  mulap0b  8647  recapb  8663  apmul1  8780  rerecapb  8835  lt2msq  8878  nnsub  8993  zltnle  9334  zleloe  9335  zrevaddcl  9338  zltp1le  9342  zapne  9362  nn0n0n1ge2b  9367  zdiv  9376  nneo  9391  zeo2  9394  qrevaddcl  9680  npnflt  9851  nmnfgt  9854  xltneg  9872  xleadd1  9911  iccid  9961  zltaddlt1le  10043  fzn  10078  0fz1  10081  uzsplit  10128  fzm1  10136  fzrevral  10141  ssfzo12bi  10261  qltnle  10282  ioo0  10296  ioom  10297  ico0  10298  ioc0  10299  flqge  10319  modqid2  10388  modqmuladd  10403  frec2uzlt2d  10441  qsqeqor  10671  nn0ltexp2  10730  shftlem  10866  shftuz  10867  caucvgrelemcau  11030  sqrtsq  11094  abs00ap  11112  cau3lem  11164  maxleb  11266  rexico  11271  negfi  11277  climshft  11353  zsumdc  11433  fsum3  11436  fsum00  11511  zproddc  11628  fprodseq  11632  dvdsval2  11838  moddvds  11847  negdvdsb  11855  dvdsnegb  11856  dvdscmulr  11868  dvdsmulcr  11869  dvdssub2  11883  fzo0dvdseq  11904  ltoddhalfle  11939  dvdsgcdb  12055  gcdzeq  12064  dvdssqlem  12072  lcmeq0  12114  lcmdvdsb  12127  coprmgcdb  12131  ncoprmgcdne1b  12132  cncongr  12148  isprm2lem  12159  dvdsprime  12165  dvdsprm  12180  coprm  12187  euclemma  12189  rpexp  12196  prmdiveq  12279  hashgcdlem  12281  odzdvds  12288  pythagtrip  12326  pcdvdsb  12363  pc2dvds  12373  pcprmpw2  12376  pcprmpw  12377  enct  12495  intopsn  12854  isgrpid2  13007  isgrpinv  13021  f1ghm0to0  13236  ringinvnz1ne0  13426  ringinvnzdiv  13427  unitmulclb  13489  dvreq1  13517  lssats2  13755  lspsneq0  13767  toponcomb  14013  tgss3  14063  isopn3  14110  neiint  14130  neipsm  14139  opnneissb  14140  opnssneib  14141  tpnei  14145  opnneiid  14149  restopnb  14166  tgcn  14193  tgcnp  14194  iscnp4  14203  cnpnei  14204  cnntr  14210  lmss  14231  upxp  14257  txcn  14260  txlm  14264  hmeoopn  14296  hmeocld  14297  xblm  14402  blssexps  14414  blssex  14415  isxms2  14437  neibl  14476  metss  14479  metrest  14491  metcnp3  14496  ivthinclemlr  14600  ivthinclemur  14602  cnplimccntop  14624  eflt  14681  lgsdir2lem4  14918  lgsne0  14925  m1lgs  14938  bj-charfunbi  15049  subctctexmid  15237  triap  15265  iswomni0  15287