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  837  nfbidf  1585  drnf1  1779  drnf2  1780  equveli  1805  ax11v2  1866  ax11v  1873  ax11ev  1874  equs5or  1876  mobidh  2111  mobid  2112  axext3  2212  cbvralfw  2754  cbvralf  2756  cbvralvw  2769  cbvraldva2  2772  gencbval  2849  vtoclgaf  2866  vtocl2gaf  2868  vtocl3gaf  2870  rspct  2900  rspc  2901  rspc2gv  2919  ceqex  2930  ralab2  2967  mob2  2983  mob  2985  morex  2987  reu7  2998  reu8  2999  nelrdva  3010  cdeqim  3021  sbcimg  3070  csbhypf  3163  cbvralcsf  3187  dfss2f  3215  sbcssg  3600  sneqrg  3840  elintab  3934  intss1  3938  intmin  3943  dfiin2g  3998  disji2  4075  disjiun  4078  trel  4189  trss  4191  bnd2  4257  zfpow  4259  exmidexmid  4280  exmidsssnc  4287  exmidundifim  4291  exmid1stab  4292  rext  4301  opth  4323  copsexg  4330  poeq1  4390  pocl  4394  swopolem  4396  swopo  4397  soeq1  4406  sowlin  4411  frforeq2  4436  frforeq3  4438  frirrg  4441  frind  4443  weeq1  4447  ordelord  4472  reusv3i  4550  ordtriexmid  4613  ontr2exmid  4617  onsucsssucexmid  4619  onsucelsucexmid  4622  ordsucunielexmid  4623  regexmidlem1  4625  regexmid  4627  reg2exmid  4628  elirr  4633  en2lp  4646  ordsoexmid  4654  onintexmid  4665  reg3exmid  4672  tfis  4675  tfisi  4679  peano2  4687  findes  4695  nnregexmid  4713  omsinds  4714  vtoclr  4767  poinxp  4788  soinxp  4789  posng  4791  ssrel  4807  ssrel2  4809  ssrelrel  4819  relop  4872  issref  5111  iotaexab  5297  iota5  5300  dffun4f  5334  sbcfung  5342  funopg  5352  brprcneu  5620  funfveu  5640  tz6.12f  5656  funbrfv  5670  ssimaexg  5696  fvmptss2  5709  fvmptssdm  5719  fvmptf  5727  fvelrn  5766  f1veqaeq  5893  dff13f  5894  isopolem  5946  isosolem  5948  riota5f  5981  imbrov2fvoveq  6026  oprabid  6033  ovmpos  6128  ov2gf  6129  ovi3  6142  caovcan  6170  caovordig  6171  caofrss  6250  caoftrn  6251  dfoprab4f  6339  f1o2ndf1  6374  poxp  6378  smoel  6446  tfrlem1  6454  tfr1onlemsucfn  6486  tfr1onlemsucaccv  6487  tfr1onlembxssdm  6489  tfr1onlembfn  6490  tfr1onlemaccex  6494  tfr1onlemres  6495  tfrcllemsucfn  6499  tfrcllemsucaccv  6500  tfrcllembxssdm  6502  tfrcllembfn  6503  tfrcllemaccex  6507  tfrcllemres  6508  tfrcl  6510  nnsucelsuc  6637  nnsucsssuc  6638  nnmordi  6662  nnaordex  6674  qsel  6759  eroveu  6773  ecopovtrn  6779  ecopovtrng  6782  th3qlem2  6785  ixpsnf1o  6883  fundmeng  6960  phplem3g  7017  nneneq  7018  ssfiexmid  7038  domfiexmid  7040  findcard  7050  findcard2  7051  findcard2s  7052  findcard2d  7053  findcard2sd  7054  diffifi  7056  ac6sfi  7060  fiintim  7093  fisseneq  7096  fidcenumlemrk  7121  fidcenumlemr  7122  isbth  7134  supeq3  7157  supeq123d  7158  supmoti  7160  suplubti  7167  supisolem  7175  cnvinfex  7185  eqinfti  7187  infvalti  7189  ordiso2  7202  nninfninc  7290  nnnninfeq2  7296  isomni  7303  finomni  7307  exmidomni  7309  ctssexmid  7317  ismkv  7320  ismkvnex  7322  mkvprop  7325  fodjumkvlemres  7326  enmkvlem  7328  iswomni  7332  exmidfodomrlemr  7380  exmidfodomrlemrALT  7381  tapeq1  7438  exmidapne  7446  ccfunen  7450  ltsonq  7585  ltexnqq  7595  prcdnql  7671  prcunqu  7672  prloc  7678  prdisj  7679  genprndl  7708  genprndu  7709  caucvgprlemnkj  7853  caucvgprlemnbj  7854  caucvgprlemcl  7863  caucvgprprlemcbv  7874  caucvgprprlemval  7875  suplocexprlemloc  7908  lttrsr  7949  ltsosr  7951  recexgt0sr  7960  mulgt0sr  7965  aptisr  7966  mulextsr1  7968  srpospr  7970  caucvgsrlemgt1  7982  caucvgsrlemoffres  7987  caucvgsr  7989  map2psrprg  7992  suplocsrlemb  7993  axprecex  8067  axpre-ltwlin  8070  axpre-lttrn  8071  axpre-apti  8072  axpre-mulgt0  8074  axpre-mulext  8075  axcaucvglemcau  8085  axcaucvglemres  8086  axpre-suploclemres  8088  axpre-suploc  8089  axsuploc  8219  ltleletr  8228  ltordlem  8629  squeeze0  9051  sup3exmid  9104  nnsub  9149  fzind  9562  uzind4s  9785  uzind4s2  9786  indstr  9788  supinfneg  9790  infsupneg  9791  frec2uzuzd  10624  frec2uzltd  10625  uzsinds  10666  seq3fveq2  10697  seqfveq2g  10699  seq3shft2  10703  seqshft2g  10704  monoord  10707  seq3split  10710  seqsplitg  10711  seqf1oglem2  10742  seqf1og  10743  seq3id2  10748  seqhomog  10752  expcl2lemap  10773  nn0ltexp2  10931  facdiv  10960  facwordi  10962  zfz1isolem1  11062  zfz1iso  11063  seq3coll  11064  wrdind  11254  wrd2ind  11255  swrdccatin1  11257  swrdccat3blem  11271  reuccatpfxs1lem  11278  caucvgre  11492  fimaxre2  11738  climcn1  11819  climcn2  11820  subcn2  11822  summodclem2a  11892  fsumsplitf  11919  fsum2d  11946  modfsummod  11969  fsumabs  11976  telfsumo  11977  fsumiun  11988  prodfdivap  12058  fprod2d  12134  fproddivapf  12142  fprodsplitf  12143  fprodsplit1f  12145  ndvdssub  12441  bezoutlemmain  12519  bezoutlemex  12522  bezoutlemzz  12523  bezoutlemsup  12530  dfgcd2  12535  algcvg  12570  algcvga  12573  algfx  12574  lcmgcdlem  12599  lcmdvds  12601  coprmgcdb  12610  coprmdvds1  12613  coprmdvds2  12615  prmind2  12642  dvdsprime  12644  nprm  12645  dvdsprm  12659  exprmfct  12660  isprm5lem  12663  coprm  12666  isprm6  12669  prmfac1  12674  sqrt2irr  12684  pcqmul  12826  pcqcl  12829  pc2dvds  12853  pcz  12855  prmpwdvds  12878  ennnfonelemim  12995  exmidunben  12997  infpn2  13027  setscomd  13073  mhmlem  13651  isnsg2  13740  ghmf1  13810  islring  14156  lringuplu  14160  rrgval  14226  rrgeq0i  14228  isdomn  14233  domneq0  14236  opprdomnbg  14238  znidom  14621  znrrg  14624  mplvalcoe  14654  mplsubgfilemcl  14663  uniopn  14675  fiinopn  14678  epttop  14764  cnpval  14872  iscnp  14873  icnpimaex  14885  lmcvg  14891  cnptoprest  14913  cnptoprest2  14914  lmss  14920  lmff  14923  txcnp  14945  txlm  14953  cnmpt12  14961  cnmpt22  14968  blssps  15101  blss  15102  metss  15168  comet  15173  metcnp3  15185  metcnp2  15187  txmetcnp  15192  divcnap  15239  mpomulcn  15240  elcncf2  15248  cncfi  15252  mulc1cncf  15263  cncfmet  15266  mulcncflem  15281  mulcncf  15282  dedekindeulemloc  15293  dedekindeulemlu  15295  dedekindeulemeu  15296  suplociccreex  15298  dedekindicclemloc  15302  dedekindicclemlu  15304  dedekindicclemeu  15305  ivthinclemlopn  15310  ivthinclemlr  15311  ivthinclemuopn  15312  ivthinclemur  15313  ivthinclemloc  15315  ivthreinc  15319  limccl  15333  ellimc3apf  15334  limccnpcntop  15349  limccnp2lem  15350  limccoap  15352  dvcoapbr  15381  dvmptfsum  15399  mpodvdsmulf1o  15664  perfectlem2  15674  lgsdir2lem4  15710  gausslemma2dlem0i  15736  lgseisenlem2  15750  lgsquad2lem2  15761  2sqlem6  15799  2sqlem8  15802  2sqlem10  15804  gropd  15848  grstructd2dom  15849  upgredg2vtx  15946  upgredgpr  15947  cbvrald  16152  bj-bdfindes  16312  bj-omtrans  16319  bj-inf2vnlem1  16333  bj-inf2vnlem2  16334  bj-inf2vnlem3  16335  bj-inf2vnlem4  16336  bj-findes  16344  strcoll2  16346  sscoll2  16351  subctctexmid  16366  pw1nct  16369  exmidsbthrlem  16390  sbthom  16394  apdiff  16416  ismkvnnlem  16420  nconstwlpolem  16433  neapmkv  16436  neap0mkv  16437  ltlenmkv  16438