Theorem imbi12d 234

Description: Deduction joining two equivalences to form equivalence of implications. (Contributed by NM, 5-Aug-1993.)

Hypotheses

Ref	Expression
imbi12d.1	|- ( ph -> ( ps <-> ch ) )
imbi12d.2	|- ( ph -> ( th <-> ta ) )

Assertion

Ref	Expression
imbi12d	|- ( ph -> ( ( ps -> th ) <-> ( ch -> ta ) ) )

Proof of Theorem imbi12d

Step	Hyp	Ref	Expression
1		imbi12d.1	. . 3 |- ( ph -> ( ps <-> ch ) )
2	1	imbi1d 231	. 2 |- ( ph -> ( ( ps -> th ) <-> ( ch -> th ) ) )
3		imbi12d.2	. . 3 |- ( ph -> ( th <-> ta ) )
4	3	imbi2d 230	. 2 |- ( ph -> ( ( ch -> th ) <-> ( ch -> ta ) ) )
5	2, 4	bitrd 188	1 |- ( ph -> ( ( ps -> th ) <-> ( ch -> ta ) ) )

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

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

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  stbid  833  nfbidf  1550  drnf1  1744  drnf2  1745  equveli  1770  ax11v2  1831  ax11v  1838  ax11ev  1839  equs5or  1841  mobidh  2076  mobid  2077  axext3  2176  cbvralfw  2716  cbvralf  2718  cbvralvw  2730  cbvraldva2  2733  gencbval  2808  vtoclgaf  2825  vtocl2gaf  2827  vtocl3gaf  2829  rspct  2857  rspc  2858  rspc2gv  2876  ceqex  2887  ralab2  2924  mob2  2940  mob  2942  morex  2944  reu7  2955  reu8  2956  nelrdva  2967  cdeqim  2978  sbcimg  3027  csbhypf  3119  cbvralcsf  3143  dfss2f  3170  sbcssg  3555  sneqrg  3788  elintab  3881  intss1  3885  intmin  3890  dfiin2g  3945  disji2  4022  disjiun  4024  trel  4134  trss  4136  bnd2  4202  zfpow  4204  exmidexmid  4225  exmidsssnc  4232  exmidundifim  4236  exmid1stab  4237  rext  4244  opth  4266  copsexg  4273  poeq1  4330  pocl  4334  swopolem  4336  swopo  4337  soeq1  4346  sowlin  4351  frforeq2  4376  frforeq3  4378  frirrg  4381  frind  4383  weeq1  4387  ordelord  4412  reusv3i  4490  ordtriexmid  4553  ontr2exmid  4557  onsucsssucexmid  4559  onsucelsucexmid  4562  ordsucunielexmid  4563  regexmidlem1  4565  regexmid  4567  reg2exmid  4568  elirr  4573  en2lp  4586  ordsoexmid  4594  onintexmid  4605  reg3exmid  4612  tfis  4615  tfisi  4619  peano2  4627  findes  4635  nnregexmid  4653  omsinds  4654  vtoclr  4707  poinxp  4728  soinxp  4729  posng  4731  ssrel  4747  ssrel2  4749  ssrelrel  4759  relop  4812  issref  5048  iotaexab  5233  iota5  5236  dffun4f  5270  sbcfung  5278  funopg  5288  brprcneu  5547  funfveu  5567  tz6.12f  5583  funbrfv  5595  ssimaexg  5619  fvmptss2  5632  fvmptssdm  5642  fvmptf  5650  fvelrn  5689  f1veqaeq  5812  dff13f  5813  isopolem  5865  isosolem  5867  riota5f  5898  imbrov2fvoveq  5943  oprabid  5950  ovmpos  6042  ov2gf  6043  ovi3  6055  caovcan  6083  caovordig  6084  caofrss  6157  caoftrn  6158  dfoprab4f  6246  f1o2ndf1  6281  poxp  6285  smoel  6353  tfrlem1  6361  tfr1onlemsucfn  6393  tfr1onlemsucaccv  6394  tfr1onlembxssdm  6396  tfr1onlembfn  6397  tfr1onlemaccex  6401  tfr1onlemres  6402  tfrcllemsucfn  6406  tfrcllemsucaccv  6407  tfrcllembxssdm  6409  tfrcllembfn  6410  tfrcllemaccex  6414  tfrcllemres  6415  tfrcl  6417  nnsucelsuc  6544  nnsucsssuc  6545  nnmordi  6569  nnaordex  6581  qsel  6666  eroveu  6680  ecopovtrn  6686  ecopovtrng  6689  th3qlem2  6692  ixpsnf1o  6790  fundmeng  6861  phplem3g  6912  nneneq  6913  ssfiexmid  6932  domfiexmid  6934  findcard  6944  findcard2  6945  findcard2s  6946  findcard2d  6947  findcard2sd  6948  diffifi  6950  ac6sfi  6954  fiintim  6985  fisseneq  6988  fidcenumlemrk  7013  fidcenumlemr  7014  isbth  7026  supeq3  7049  supeq123d  7050  supmoti  7052  suplubti  7059  supisolem  7067  cnvinfex  7077  eqinfti  7079  infvalti  7081  ordiso2  7094  nninfninc  7182  nnnninfeq2  7188  isomni  7195  finomni  7199  exmidomni  7201  ctssexmid  7209  ismkv  7212  ismkvnex  7214  mkvprop  7217  fodjumkvlemres  7218  enmkvlem  7220  iswomni  7224  exmidfodomrlemr  7262  exmidfodomrlemrALT  7263  tapeq1  7312  exmidapne  7320  ccfunen  7324  ltsonq  7458  ltexnqq  7468  prcdnql  7544  prcunqu  7545  prloc  7551  prdisj  7552  genprndl  7581  genprndu  7582  caucvgprlemnkj  7726  caucvgprlemnbj  7727  caucvgprlemcl  7736  caucvgprprlemcbv  7747  caucvgprprlemval  7748  suplocexprlemloc  7781  lttrsr  7822  ltsosr  7824  recexgt0sr  7833  mulgt0sr  7838  aptisr  7839  mulextsr1  7841  srpospr  7843  caucvgsrlemgt1  7855  caucvgsrlemoffres  7860  caucvgsr  7862  map2psrprg  7865  suplocsrlemb  7866  axprecex  7940  axpre-ltwlin  7943  axpre-lttrn  7944  axpre-apti  7945  axpre-mulgt0  7947  axpre-mulext  7948  axcaucvglemcau  7958  axcaucvglemres  7959  axpre-suploclemres  7961  axpre-suploc  7962  axsuploc  8092  ltleletr  8101  ltordlem  8501  squeeze0  8923  sup3exmid  8976  nnsub  9021  fzind  9432  uzind4s  9655  uzind4s2  9656  indstr  9658  supinfneg  9660  infsupneg  9661  frec2uzuzd  10473  frec2uzltd  10474  uzsinds  10515  seq3fveq2  10546  seqfveq2g  10548  seq3shft2  10552  seqshft2g  10553  monoord  10556  seq3split  10559  seqsplitg  10560  seqf1oglem2  10591  seqf1og  10592  seq3id2  10597  seqhomog  10601  expcl2lemap  10622  nn0ltexp2  10780  facdiv  10809  facwordi  10811  zfz1isolem1  10911  zfz1iso  10912  seq3coll  10913  caucvgre  11125  fimaxre2  11370  climcn1  11451  climcn2  11452  subcn2  11454  summodclem2a  11524  fsumsplitf  11551  fsum2d  11578  modfsummod  11601  fsumabs  11608  telfsumo  11609  fsumiun  11620  prodfdivap  11690  fprod2d  11766  fproddivapf  11774  fprodsplitf  11775  fprodsplit1f  11777  ndvdssub  12071  bezoutlemmain  12135  bezoutlemex  12138  bezoutlemzz  12139  bezoutlemsup  12146  dfgcd2  12151  algcvg  12186  algcvga  12189  algfx  12190  lcmgcdlem  12215  lcmdvds  12217  coprmgcdb  12226  coprmdvds1  12229  coprmdvds2  12231  prmind2  12258  dvdsprime  12260  nprm  12261  dvdsprm  12275  exprmfct  12276  isprm5lem  12279  coprm  12282  isprm6  12285  prmfac1  12290  sqrt2irr  12300  pcqmul  12441  pcqcl  12444  pc2dvds  12468  pcz  12470  prmpwdvds  12493  ennnfonelemim  12581  exmidunben  12583  infpn2  12613  setscomd  12659  mhmlem  13184  isnsg2  13273  ghmf1  13343  islring  13688  lringuplu  13692  rrgval  13758  rrgeq0i  13760  isdomn  13765  domneq0  13768  opprdomnbg  13770  znidom  14145  znrrg  14148  uniopn  14169  fiinopn  14172  epttop  14258  cnpval  14366  iscnp  14367  icnpimaex  14379  lmcvg  14385  cnptoprest  14407  cnptoprest2  14408  lmss  14414  lmff  14417  txcnp  14439  txlm  14447  cnmpt12  14455  cnmpt22  14462  blssps  14595  blss  14596  metss  14662  comet  14667  metcnp3  14679  metcnp2  14681  txmetcnp  14686  divcnap  14723  elcncf2  14729  cncfi  14733  mulc1cncf  14744  cncfmet  14747  mulcncflem  14761  mulcncf  14762  dedekindeulemloc  14773  dedekindeulemlu  14775  dedekindeulemeu  14776  suplociccreex  14778  dedekindicclemloc  14782  dedekindicclemlu  14784  dedekindicclemeu  14785  ivthinclemlopn  14790  ivthinclemlr  14791  ivthinclemuopn  14792  ivthinclemur  14793  ivthinclemloc  14795  ivthreinc  14799  limccl  14813  ellimc3apf  14814  limccnpcntop  14829  limccnp2lem  14830  limccoap  14832  dvcoapbr  14856  lgsdir2lem4  15147  gausslemma2dlem0i  15173  lgseisenlem2  15187  2sqlem6  15207  2sqlem8  15210  2sqlem10  15212  cbvrald  15280  bj-bdfindes  15441  bj-omtrans  15448  bj-inf2vnlem1  15462  bj-inf2vnlem2  15463  bj-inf2vnlem3  15464  bj-inf2vnlem4  15465  bj-findes  15473  strcoll2  15475  sscoll2  15480  subctctexmid  15491  pw1nct  15493  exmidsbthrlem  15512  sbthom  15516  apdiff  15538  ismkvnnlem  15542  nconstwlpolem  15555  neapmkv  15558  neap0mkv  15559  ltlenmkv  15560