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  1553  drnf1  1747  drnf2  1748  equveli  1773  ax11v2  1834  ax11v  1841  ax11ev  1842  equs5or  1844  mobidh  2079  mobid  2080  axext3  2179  cbvralfw  2719  cbvralf  2721  cbvralvw  2733  cbvraldva2  2736  gencbval  2812  vtoclgaf  2829  vtocl2gaf  2831  vtocl3gaf  2833  rspct  2861  rspc  2862  rspc2gv  2880  ceqex  2891  ralab2  2928  mob2  2944  mob  2946  morex  2948  reu7  2959  reu8  2960  nelrdva  2971  cdeqim  2982  sbcimg  3031  csbhypf  3123  cbvralcsf  3147  dfss2f  3175  sbcssg  3560  sneqrg  3793  elintab  3886  intss1  3890  intmin  3895  dfiin2g  3950  disji2  4027  disjiun  4029  trel  4139  trss  4141  bnd2  4207  zfpow  4209  exmidexmid  4230  exmidsssnc  4237  exmidundifim  4241  exmid1stab  4242  rext  4249  opth  4271  copsexg  4278  poeq1  4335  pocl  4339  swopolem  4341  swopo  4342  soeq1  4351  sowlin  4356  frforeq2  4381  frforeq3  4383  frirrg  4386  frind  4388  weeq1  4392  ordelord  4417  reusv3i  4495  ordtriexmid  4558  ontr2exmid  4562  onsucsssucexmid  4564  onsucelsucexmid  4567  ordsucunielexmid  4568  regexmidlem1  4570  regexmid  4572  reg2exmid  4573  elirr  4578  en2lp  4591  ordsoexmid  4599  onintexmid  4610  reg3exmid  4617  tfis  4620  tfisi  4624  peano2  4632  findes  4640  nnregexmid  4658  omsinds  4659  vtoclr  4712  poinxp  4733  soinxp  4734  posng  4736  ssrel  4752  ssrel2  4754  ssrelrel  4764  relop  4817  issref  5053  iotaexab  5238  iota5  5241  dffun4f  5275  sbcfung  5283  funopg  5293  brprcneu  5554  funfveu  5574  tz6.12f  5590  funbrfv  5602  ssimaexg  5626  fvmptss2  5639  fvmptssdm  5649  fvmptf  5657  fvelrn  5696  f1veqaeq  5819  dff13f  5820  isopolem  5872  isosolem  5874  riota5f  5905  imbrov2fvoveq  5950  oprabid  5957  ovmpos  6050  ov2gf  6051  ovi3  6064  caovcan  6092  caovordig  6093  caofrss  6171  caoftrn  6172  dfoprab4f  6260  f1o2ndf1  6295  poxp  6299  smoel  6367  tfrlem1  6375  tfr1onlemsucfn  6407  tfr1onlemsucaccv  6408  tfr1onlembxssdm  6410  tfr1onlembfn  6411  tfr1onlemaccex  6415  tfr1onlemres  6416  tfrcllemsucfn  6420  tfrcllemsucaccv  6421  tfrcllembxssdm  6423  tfrcllembfn  6424  tfrcllemaccex  6428  tfrcllemres  6429  tfrcl  6431  nnsucelsuc  6558  nnsucsssuc  6559  nnmordi  6583  nnaordex  6595  qsel  6680  eroveu  6694  ecopovtrn  6700  ecopovtrng  6703  th3qlem2  6706  ixpsnf1o  6804  fundmeng  6875  phplem3g  6926  nneneq  6927  ssfiexmid  6946  domfiexmid  6948  findcard  6958  findcard2  6959  findcard2s  6960  findcard2d  6961  findcard2sd  6962  diffifi  6964  ac6sfi  6968  fiintim  7001  fisseneq  7004  fidcenumlemrk  7029  fidcenumlemr  7030  isbth  7042  supeq3  7065  supeq123d  7066  supmoti  7068  suplubti  7075  supisolem  7083  cnvinfex  7093  eqinfti  7095  infvalti  7097  ordiso2  7110  nninfninc  7198  nnnninfeq2  7204  isomni  7211  finomni  7215  exmidomni  7217  ctssexmid  7225  ismkv  7228  ismkvnex  7230  mkvprop  7233  fodjumkvlemres  7234  enmkvlem  7236  iswomni  7240  exmidfodomrlemr  7283  exmidfodomrlemrALT  7284  tapeq1  7337  exmidapne  7345  ccfunen  7349  ltsonq  7484  ltexnqq  7494  prcdnql  7570  prcunqu  7571  prloc  7577  prdisj  7578  genprndl  7607  genprndu  7608  caucvgprlemnkj  7752  caucvgprlemnbj  7753  caucvgprlemcl  7762  caucvgprprlemcbv  7773  caucvgprprlemval  7774  suplocexprlemloc  7807  lttrsr  7848  ltsosr  7850  recexgt0sr  7859  mulgt0sr  7864  aptisr  7865  mulextsr1  7867  srpospr  7869  caucvgsrlemgt1  7881  caucvgsrlemoffres  7886  caucvgsr  7888  map2psrprg  7891  suplocsrlemb  7892  axprecex  7966  axpre-ltwlin  7969  axpre-lttrn  7970  axpre-apti  7971  axpre-mulgt0  7973  axpre-mulext  7974  axcaucvglemcau  7984  axcaucvglemres  7985  axpre-suploclemres  7987  axpre-suploc  7988  axsuploc  8118  ltleletr  8127  ltordlem  8528  squeeze0  8950  sup3exmid  9003  nnsub  9048  fzind  9460  uzind4s  9683  uzind4s2  9684  indstr  9686  supinfneg  9688  infsupneg  9689  frec2uzuzd  10513  frec2uzltd  10514  uzsinds  10555  seq3fveq2  10586  seqfveq2g  10588  seq3shft2  10592  seqshft2g  10593  monoord  10596  seq3split  10599  seqsplitg  10600  seqf1oglem2  10631  seqf1og  10632  seq3id2  10637  seqhomog  10641  expcl2lemap  10662  nn0ltexp2  10820  facdiv  10849  facwordi  10851  zfz1isolem1  10951  zfz1iso  10952  seq3coll  10953  caucvgre  11165  fimaxre2  11411  climcn1  11492  climcn2  11493  subcn2  11495  summodclem2a  11565  fsumsplitf  11592  fsum2d  11619  modfsummod  11642  fsumabs  11649  telfsumo  11650  fsumiun  11661  prodfdivap  11731  fprod2d  11807  fproddivapf  11815  fprodsplitf  11816  fprodsplit1f  11818  ndvdssub  12114  bezoutlemmain  12192  bezoutlemex  12195  bezoutlemzz  12196  bezoutlemsup  12203  dfgcd2  12208  algcvg  12243  algcvga  12246  algfx  12247  lcmgcdlem  12272  lcmdvds  12274  coprmgcdb  12283  coprmdvds1  12286  coprmdvds2  12288  prmind2  12315  dvdsprime  12317  nprm  12318  dvdsprm  12332  exprmfct  12333  isprm5lem  12336  coprm  12339  isprm6  12342  prmfac1  12347  sqrt2irr  12357  pcqmul  12499  pcqcl  12502  pc2dvds  12526  pcz  12528  prmpwdvds  12551  ennnfonelemim  12668  exmidunben  12670  infpn2  12700  setscomd  12746  mhmlem  13322  isnsg2  13411  ghmf1  13481  islring  13826  lringuplu  13830  rrgval  13896  rrgeq0i  13898  isdomn  13903  domneq0  13906  opprdomnbg  13908  znidom  14291  znrrg  14294  mplvalcoe  14324  mplsubgfilemcl  14333  uniopn  14345  fiinopn  14348  epttop  14434  cnpval  14542  iscnp  14543  icnpimaex  14555  lmcvg  14561  cnptoprest  14583  cnptoprest2  14584  lmss  14590  lmff  14593  txcnp  14615  txlm  14623  cnmpt12  14631  cnmpt22  14638  blssps  14771  blss  14772  metss  14838  comet  14843  metcnp3  14855  metcnp2  14857  txmetcnp  14862  divcnap  14909  mpomulcn  14910  elcncf2  14918  cncfi  14922  mulc1cncf  14933  cncfmet  14936  mulcncflem  14951  mulcncf  14952  dedekindeulemloc  14963  dedekindeulemlu  14965  dedekindeulemeu  14966  suplociccreex  14968  dedekindicclemloc  14972  dedekindicclemlu  14974  dedekindicclemeu  14975  ivthinclemlopn  14980  ivthinclemlr  14981  ivthinclemuopn  14982  ivthinclemur  14983  ivthinclemloc  14985  ivthreinc  14989  limccl  15003  ellimc3apf  15004  limccnpcntop  15019  limccnp2lem  15020  limccoap  15022  dvcoapbr  15051  dvmptfsum  15069  mpodvdsmulf1o  15334  perfectlem2  15344  lgsdir2lem4  15380  gausslemma2dlem0i  15406  lgseisenlem2  15420  lgsquad2lem2  15431  2sqlem6  15469  2sqlem8  15472  2sqlem10  15474  cbvrald  15542  bj-bdfindes  15703  bj-omtrans  15710  bj-inf2vnlem1  15724  bj-inf2vnlem2  15725  bj-inf2vnlem3  15726  bj-inf2vnlem4  15727  bj-findes  15735  strcoll2  15737  sscoll2  15742  subctctexmid  15755  pw1nct  15758  exmidsbthrlem  15779  sbthom  15783  apdiff  15805  ismkvnnlem  15809  nconstwlpolem  15822  neapmkv  15825  neap0mkv  15826  ltlenmkv  15827