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  5622  funfveu  5642  tz6.12f  5658  funbrfv  5672  ssimaexg  5698  fvmptss2  5711  fvmptssdm  5721  fvmptf  5729  fvelrn  5768  f1veqaeq  5899  dff13f  5900  isopolem  5952  isosolem  5954  riota5f  5987  imbrov2fvoveq  6032  oprabid  6039  ovmpos  6134  ov2gf  6135  ovi3  6148  caovcan  6176  caovordig  6177  caofrss  6256  caoftrn  6257  dfoprab4f  6345  f1o2ndf1  6380  poxp  6384  smoel  6452  tfrlem1  6460  tfr1onlemsucfn  6492  tfr1onlemsucaccv  6493  tfr1onlembxssdm  6495  tfr1onlembfn  6496  tfr1onlemaccex  6500  tfr1onlemres  6501  tfrcllemsucfn  6505  tfrcllemsucaccv  6506  tfrcllembxssdm  6508  tfrcllembfn  6509  tfrcllemaccex  6513  tfrcllemres  6514  tfrcl  6516  nnsucelsuc  6645  nnsucsssuc  6646  nnmordi  6670  nnaordex  6682  qsel  6767  eroveu  6781  ecopovtrn  6787  ecopovtrng  6790  th3qlem2  6793  ixpsnf1o  6891  fundmeng  6968  phplem3g  7025  nneneq  7026  ssfiexmid  7046  domfiexmid  7048  findcard  7058  findcard2  7059  findcard2s  7060  findcard2d  7061  findcard2sd  7062  diffifi  7064  ac6sfi  7068  fiintim  7104  fisseneq  7107  fidcenumlemrk  7132  fidcenumlemr  7133  isbth  7145  supeq3  7168  supeq123d  7169  supmoti  7171  suplubti  7178  supisolem  7186  cnvinfex  7196  eqinfti  7198  infvalti  7200  ordiso2  7213  nninfninc  7301  nnnninfeq2  7307  isomni  7314  finomni  7318  exmidomni  7320  ctssexmid  7328  ismkv  7331  ismkvnex  7333  mkvprop  7336  fodjumkvlemres  7337  enmkvlem  7339  iswomni  7343  exmidfodomrlemr  7391  exmidfodomrlemrALT  7392  tapeq1  7449  exmidapne  7457  ccfunen  7461  ltsonq  7596  ltexnqq  7606  prcdnql  7682  prcunqu  7683  prloc  7689  prdisj  7690  genprndl  7719  genprndu  7720  caucvgprlemnkj  7864  caucvgprlemnbj  7865  caucvgprlemcl  7874  caucvgprprlemcbv  7885  caucvgprprlemval  7886  suplocexprlemloc  7919  lttrsr  7960  ltsosr  7962  recexgt0sr  7971  mulgt0sr  7976  aptisr  7977  mulextsr1  7979  srpospr  7981  caucvgsrlemgt1  7993  caucvgsrlemoffres  7998  caucvgsr  8000  map2psrprg  8003  suplocsrlemb  8004  axprecex  8078  axpre-ltwlin  8081  axpre-lttrn  8082  axpre-apti  8083  axpre-mulgt0  8085  axpre-mulext  8086  axcaucvglemcau  8096  axcaucvglemres  8097  axpre-suploclemres  8099  axpre-suploc  8100  axsuploc  8230  ltleletr  8239  ltordlem  8640  squeeze0  9062  sup3exmid  9115  nnsub  9160  fzind  9573  uzind4s  9797  uzind4s2  9798  indstr  9800  supinfneg  9802  infsupneg  9803  frec2uzuzd  10636  frec2uzltd  10637  uzsinds  10678  seq3fveq2  10709  seqfveq2g  10711  seq3shft2  10715  seqshft2g  10716  monoord  10719  seq3split  10722  seqsplitg  10723  seqf1oglem2  10754  seqf1og  10755  seq3id2  10760  seqhomog  10764  expcl2lemap  10785  nn0ltexp2  10943  facdiv  10972  facwordi  10974  zfz1isolem1  11075  zfz1iso  11076  seq3coll  11077  wrdind  11269  wrd2ind  11270  swrdccatin1  11272  swrdccat3blem  11286  reuccatpfxs1lem  11293  caucvgre  11507  fimaxre2  11753  climcn1  11834  climcn2  11835  subcn2  11837  summodclem2a  11907  fsumsplitf  11934  fsum2d  11961  modfsummod  11984  fsumabs  11991  telfsumo  11992  fsumiun  12003  prodfdivap  12073  fprod2d  12149  fproddivapf  12157  fprodsplitf  12158  fprodsplit1f  12160  ndvdssub  12456  bezoutlemmain  12534  bezoutlemex  12537  bezoutlemzz  12538  bezoutlemsup  12545  dfgcd2  12550  algcvg  12585  algcvga  12588  algfx  12589  lcmgcdlem  12614  lcmdvds  12616  coprmgcdb  12625  coprmdvds1  12628  coprmdvds2  12630  prmind2  12657  dvdsprime  12659  nprm  12660  dvdsprm  12674  exprmfct  12675  isprm5lem  12678  coprm  12681  isprm6  12684  prmfac1  12689  sqrt2irr  12699  pcqmul  12841  pcqcl  12844  pc2dvds  12868  pcz  12870  prmpwdvds  12893  ennnfonelemim  13010  exmidunben  13012  infpn2  13042  setscomd  13088  mhmlem  13666  isnsg2  13755  ghmf1  13825  islring  14171  lringuplu  14175  rrgval  14241  rrgeq0i  14243  isdomn  14248  domneq0  14251  opprdomnbg  14253  znidom  14636  znrrg  14639  mplvalcoe  14669  mplsubgfilemcl  14678  uniopn  14690  fiinopn  14693  epttop  14779  cnpval  14887  iscnp  14888  icnpimaex  14900  lmcvg  14906  cnptoprest  14928  cnptoprest2  14929  lmss  14935  lmff  14938  txcnp  14960  txlm  14968  cnmpt12  14976  cnmpt22  14983  blssps  15116  blss  15117  metss  15183  comet  15188  metcnp3  15200  metcnp2  15202  txmetcnp  15207  divcnap  15254  mpomulcn  15255  elcncf2  15263  cncfi  15267  mulc1cncf  15278  cncfmet  15281  mulcncflem  15296  mulcncf  15297  dedekindeulemloc  15308  dedekindeulemlu  15310  dedekindeulemeu  15311  suplociccreex  15313  dedekindicclemloc  15317  dedekindicclemlu  15319  dedekindicclemeu  15320  ivthinclemlopn  15325  ivthinclemlr  15326  ivthinclemuopn  15327  ivthinclemur  15328  ivthinclemloc  15330  ivthreinc  15334  limccl  15348  ellimc3apf  15349  limccnpcntop  15364  limccnp2lem  15365  limccoap  15367  dvcoapbr  15396  dvmptfsum  15414  mpodvdsmulf1o  15679  perfectlem2  15689  lgsdir2lem4  15725  gausslemma2dlem0i  15751  lgseisenlem2  15765  lgsquad2lem2  15776  2sqlem6  15814  2sqlem8  15817  2sqlem10  15819  gropd  15863  grstructd2dom  15864  upgredg2vtx  15961  upgredgpr  15962  cbvrald  16207  bj-bdfindes  16367  bj-omtrans  16374  bj-inf2vnlem1  16388  bj-inf2vnlem2  16389  bj-inf2vnlem3  16390  bj-inf2vnlem4  16391  bj-findes  16399  strcoll2  16401  sscoll2  16406  subctctexmid  16425  pw1nct  16428  exmidsbthrlem  16450  sbthom  16454  apdiff  16476  ismkvnnlem  16480  nconstwlpolem  16493  neapmkv  16496  neap0mkv  16497  ltlenmkv  16498