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  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  4108  disjeq1  4111  exmidsssnc  4338  copsexg  4382  euotd  4393  poeq2  4443  sotritric  4467  sotritrieq  4468  seeq1  4482  seeq2  4483  alxfr  4605  ralxfrd  4606  rexxfrd  4607  ordelsuc  4650  sosng  4846  iss  5107  iotaval  5347  funeq  5395  funssres  5418  f0dom0  5584  tz6.12c  5723  fnbrfvb  5738  ssimaex  5761  fvimacnv  5818  elpreima  5822  fsn  5874  fconst2g  5924  fndmexb  5932  elunirn  5966  f1ocnvfvb  5980  foeqcnvco  5990  f1eqcocnv  5991  fliftfun  5996  isose  6021  isopo  6023  isoso  6025  f1oiso2  6027  eusvobj2  6065  oprabid  6111  f1opw2  6290  op1steq  6407  fvn0elsuppb  6486  rntpos  6522  frecabcl  6664  nnsucelsuc  6758  nnsucsssuc  6759  nnsseleq  6768  nnaord  6776  nnmord  6784  nnaordex  6795  nnawordex  6796  nnm00  6797  erexb  6826  swoord1  6830  swoord2  6831  iinerm  6875  mapsnd  6964  fundmen  7088  dom1o  7110  mapxpen  7142  mapunen  7145  ssenen  7146  nneneq  7152  nndomo  7159  fidifsnen  7166  en1eqsnbi  7260  suplub2ti  7335  isoti  7341  ordiso2  7369  ordiso  7370  ctm  7443  ctssdc  7447  enomni  7473  enmkv  7496  enwomni  7504  pm54.43  7530  pr2ne  7532  ltexnqq  7769  genprndl  7882  genprndu  7883  nqprl  7912  nqpru  7913  1idprl  7951  1idpru  7952  ltexprlemrnd  7966  ltaprg  7980  recexprlemrnd  7990  cauappcvgprlemrnd  8011  caucvgprlemrnd  8034  caucvgprprlemrnd  8062  suplocexprlemrl  8078  suplocexprlemru  8080  map2psrprg  8166  ltxrlt  8385  lttri3  8399  addlsub  8690  addid0  8693  ltadd2  8741  eqord1  8805  reapti  8901  apreap  8909  ltmul1  8914  apreim  8925  ltleap  8954  mulap0b  8977  recapb  8995  apmul1  9112  rerecapb  9167  lt2msq  9210  nnsub  9326  zltnle  9673  zleloe  9674  zrevaddcl  9678  zltp1le  9682  zapne  9702  nn0n0n1ge2b  9708  zdiv  9717  nneo  9732  zeo2  9735  qrevaddcl  10027  npnflt  10200  nmnfgt  10203  xltneg  10221  xleadd1  10260  iccid  10310  zltaddlt1le  10393  fzn  10429  0fz1  10432  uzsplit  10482  fzm1  10490  fzrevral  10495  ssfzo12bi  10626  qltnle  10661  ioo0  10677  ioom  10678  ico0  10679  ioc0  10680  flqge  10700  modqid2  10771  modqmuladd  10786  frec2uzlt2d  10824  seqf1oglem1  10939  qsqeqor  11070  nn0ltexp2  11130  hashtpg  11282  len0nnbi  11322  ccats1pfxeqbi  11497  reuccatpfxs1  11502  shftlem  11564  shftuz  11565  caucvgrelemcau  11729  sqrtsq  11793  abs00ap  11811  cau3lem  11863  maxleb  11965  rexico  11970  negfi  11977  climshft  12053  zsumdc  12134  fsum3  12137  fsum00  12212  zproddc  12329  fprodseq  12333  dvdsval2  12540  moddvds  12549  negdvdsb  12557  dvdsnegb  12558  dvdscmulr  12570  dvdsmulcr  12571  dvdssub2  12585  fzo0dvdseq  12607  ltoddhalfle  12643  dvdsgcdb  12773  gcdzeq  12782  dvdssqlem  12790  lcmeq0  12832  lcmdvdsb  12845  coprmgcdb  12849  ncoprmgcdne1b  12850  cncongr  12866  isprm2lem  12877  dvdsprime  12883  dvdsprm  12898  coprm  12905  euclemma  12907  rpexp  12914  prmdiveq  12997  hashgcdlem  12999  odzdvds  13007  pythagtrip  13045  pcdvdsb  13082  pc2dvds  13092  pcprmpw2  13095  pcprmpw  13096  enct  13307  intopsn  13670  gzsumfzval  13694  isgrpid2  13828  isgrpinv  13842  f1ghm0to0  14058  ringinvnz1ne0  14337  ringinvnzdiv  14338  unitmulclb  14404  dvreq1  14432  isnzr2  14474  rrgeq0  14556  domneq0  14564  lssats2  14734  lspsneq0  14746  znunit  14977  toponcomb  15112  tgss3  15162  isopn3  15209  neiint  15229  neipsm  15238  opnneissb  15239  opnssneib  15240  tpnei  15244  opnneiid  15248  restopnb  15265  tgcn  15292  tgcnp  15293  iscnp4  15302  cnpnei  15303  cnntr  15309  lmss  15330  upxp  15356  txcn  15359  txlm  15363  hmeoopn  15395  hmeocld  15396  xblm  15501  blssexps  15513  blssex  15514  isxms2  15536  neibl  15575  metss  15578  metrest  15590  metcnp3  15595  ivthinclemlr  15721  ivthinclemur  15723  cnplimccntop  15754  eflt  15859  dvdsppwf1o  16086  lgsdir2lem4  16133  lgsne0  16140  gausslemma2dlem1a  16160  lgsquadlem1  16179  m1lgs  16187  uhgr0vb  16308  ausgrusgrben  16392  ushgredgedg  16450  ushgredgedgloop  16452  usgr0vb  16457  loopclwwlkn1b  16643  eupth2lem3lem4fi  16697  lealltlt1  16734  lealltlt2  16735  bj-charfunbi  16820  subctctexmid  17013  triap  17052  iswomni0  17075  alsralrex  17127