Theorem impbid 128

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 127	. 2 |- ( ph -> ( ph -> ( ps <-> ch ) ) )
4	3	pm2.43i 49	1 |- ( ph -> ( ps <-> ch ) )

Syntax hints:   -> wi 4   <-> wb 104

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia2 106  ax-ia3 107

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  bicom1  130  impbid1  141  pm5.74  178  imbi1d  230  pm5.501  243  pm5.32d  447  impbida  591  notbi  661  pm5.21  690  nbn2  692  2falsed  697  pm5.21ndd  700  oibabs  709  orbi2d  785  con4biddc  852  con1bidc  869  con1bdc  873  dedlema  964  dedlemb  965  xorbin  1379  albi  1461  19.21ht  1574  exbi  1597  19.23t  1670  equequ1  1705  equequ2  1706  equsexd  1722  dral1  1723  cbv2h  1741  cbv2w  1743  sbequ12  1764  sbiedh  1780  drex1  1791  ax11b  1819  sbequ  1833  sbft  1841  sb56  1878  cbvexdh  1919  eupickb  2100  eupickbi  2101  elequ1  2145  elequ2  2146  ceqsalt  2756  ceqex  2857  mob2  2910  euxfr2dc  2915  reu6  2919  sbciegft  2985  csbiebt  3088  sseq1  3170  reupick  3411  reupick2  3413  disjeq2  3970  disjeq1  3973  exmidsssnc  4189  copsexg  4229  euotd  4239  poeq2  4285  sotritric  4309  sotritrieq  4310  seeq1  4324  seeq2  4325  alxfr  4446  ralxfrd  4447  rexxfrd  4448  ordelsuc  4489  sosng  4684  iss  4937  iotaval  5171  funeq  5218  funssres  5240  f0dom0  5391  tz6.12c  5526  fnbrfvb  5537  ssimaex  5557  fvimacnv  5611  elpreima  5615  fsn  5668  fconst2g  5711  elunirn  5745  f1ocnvfvb  5759  foeqcnvco  5769  f1eqcocnv  5770  fliftfun  5775  isose  5800  isopo  5802  isoso  5804  f1oiso2  5806  eusvobj2  5839  oprabid  5885  f1opw2  6055  op1steq  6158  rntpos  6236  frecabcl  6378  nnsucelsuc  6470  nnsucsssuc  6471  nnsseleq  6480  nnaord  6488  nnmord  6496  nnaordex  6507  nnawordex  6508  nnm00  6509  erexb  6538  swoord1  6542  swoord2  6543  iinerm  6585  fundmen  6784  mapxpen  6826  ssenen  6829  nneneq  6835  nndomo  6842  fidifsnen  6848  en1eqsnbi  6926  suplub2ti  6978  isoti  6984  ordiso2  7012  ordiso  7013  ctm  7086  ctssdc  7090  enomni  7115  enmkv  7138  enwomni  7146  pm54.43  7167  pr2ne  7169  ltexnqq  7370  genprndl  7483  genprndu  7484  nqprl  7513  nqpru  7514  1idprl  7552  1idpru  7553  ltexprlemrnd  7567  ltaprg  7581  recexprlemrnd  7591  cauappcvgprlemrnd  7612  caucvgprlemrnd  7635  caucvgprprlemrnd  7663  suplocexprlemrl  7679  suplocexprlemru  7681  map2psrprg  7767  ltxrlt  7985  lttri3  7999  addlsub  8289  addid0  8292  ltadd2  8338  eqord1  8402  reapti  8498  apreap  8506  ltmul1  8511  apreim  8522  ltleap  8551  mulap0b  8573  apmul1  8705  lt2msq  8802  nnsub  8917  zltnle  9258  zleloe  9259  zrevaddcl  9262  zltp1le  9266  zapne  9286  nn0n0n1ge2b  9291  zdiv  9300  nneo  9315  zeo2  9318  qrevaddcl  9603  npnflt  9772  nmnfgt  9775  xltneg  9793  xleadd1  9832  iccid  9882  zltaddlt1le  9964  fzn  9998  0fz1  10001  uzsplit  10048  fzm1  10056  fzrevral  10061  ssfzo12bi  10181  qltnle  10202  ioo0  10216  ioom  10217  ico0  10218  ioc0  10219  flqge  10238  modqid2  10307  modqmuladd  10322  frec2uzlt2d  10360  qsqeqor  10586  nn0ltexp2  10644  shftlem  10780  shftuz  10781  caucvgrelemcau  10944  sqrtsq  11008  abs00ap  11026  cau3lem  11078  maxleb  11180  rexico  11185  negfi  11191  climshft  11267  zsumdc  11347  fsum3  11350  fsum00  11425  zproddc  11542  fprodseq  11546  dvdsval2  11752  moddvds  11761  negdvdsb  11769  dvdsnegb  11770  dvdscmulr  11782  dvdsmulcr  11783  dvdssub2  11797  fzo0dvdseq  11817  ltoddhalfle  11852  dvdsgcdb  11968  gcdzeq  11977  dvdssqlem  11985  lcmeq0  12025  lcmdvdsb  12038  coprmgcdb  12042  ncoprmgcdne1b  12043  cncongr  12059  isprm2lem  12070  dvdsprime  12076  dvdsprm  12091  coprm  12098  euclemma  12100  rpexp  12107  prmdiveq  12190  hashgcdlem  12192  odzdvds  12199  pythagtrip  12237  pcdvdsb  12273  pc2dvds  12283  pcprmpw2  12286  pcprmpw  12287  enct  12388  intopsn  12621  isgrpid2  12743  isgrpinv  12756  toponcomb  12820  tgss3  12872  isopn3  12919  neiint  12939  neipsm  12948  opnneissb  12949  opnssneib  12950  tpnei  12954  opnneiid  12958  restopnb  12975  tgcn  13002  tgcnp  13003  iscnp4  13012  cnpnei  13013  cnntr  13019  lmss  13040  upxp  13066  txcn  13069  txlm  13073  hmeoopn  13105  hmeocld  13106  xblm  13211  blssexps  13223  blssex  13224  isxms2  13246  neibl  13285  metss  13288  metrest  13300  metcnp3  13305  ivthinclemlr  13409  ivthinclemur  13411  cnplimccntop  13433  eflt  13490  lgsdir2lem4  13726  lgsne0  13733  bj-charfunbi  13846  subctctexmid  14034  triap  14061  iswomni0  14083