Theorem imbi12d 234

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

Hypotheses

Ref	Expression
imbi12d.1	⊢ (𝜑 → (𝜓 ↔ 𝜒))
imbi12d.2	⊢ (𝜑 → (𝜃 ↔ 𝜏))

Assertion

Ref	Expression
imbi12d	⊢ (𝜑 → ((𝜓 → 𝜃) ↔ (𝜒 → 𝜏)))

Proof of Theorem imbi12d

Step	Hyp	Ref	Expression
1		imbi12d.1	. . 3 ⊢ (𝜑 → (𝜓 ↔ 𝜒))
2	1	imbi1d 231	. 2 ⊢ (𝜑 → ((𝜓 → 𝜃) ↔ (𝜒 → 𝜃)))
3		imbi12d.2	. . 3 ⊢ (𝜑 → (𝜃 ↔ 𝜏))
4	3	imbi2d 230	. 2 ⊢ (𝜑 → ((𝜒 → 𝜃) ↔ (𝜒 → 𝜏)))
5	2, 4	bitrd 188	1 ⊢ (𝜑 → ((𝜓 → 𝜃) ↔ (𝜒 → 𝜏)))

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  7281  exmidfodomrlemrALT  7282  tapeq1  7335  exmidapne  7343  ccfunen  7347  ltsonq  7482  ltexnqq  7492  prcdnql  7568  prcunqu  7569  prloc  7575  prdisj  7576  genprndl  7605  genprndu  7606  caucvgprlemnkj  7750  caucvgprlemnbj  7751  caucvgprlemcl  7760  caucvgprprlemcbv  7771  caucvgprprlemval  7772  suplocexprlemloc  7805  lttrsr  7846  ltsosr  7848  recexgt0sr  7857  mulgt0sr  7862  aptisr  7863  mulextsr1  7865  srpospr  7867  caucvgsrlemgt1  7879  caucvgsrlemoffres  7884  caucvgsr  7886  map2psrprg  7889  suplocsrlemb  7890  axprecex  7964  axpre-ltwlin  7967  axpre-lttrn  7968  axpre-apti  7969  axpre-mulgt0  7971  axpre-mulext  7972  axcaucvglemcau  7982  axcaucvglemres  7983  axpre-suploclemres  7985  axpre-suploc  7986  axsuploc  8116  ltleletr  8125  ltordlem  8526  squeeze0  8948  sup3exmid  9001  nnsub  9046  fzind  9458  uzind4s  9681  uzind4s2  9682  indstr  9684  supinfneg  9686  infsupneg  9687  frec2uzuzd  10511  frec2uzltd  10512  uzsinds  10553  seq3fveq2  10584  seqfveq2g  10586  seq3shft2  10590  seqshft2g  10591  monoord  10594  seq3split  10597  seqsplitg  10598  seqf1oglem2  10629  seqf1og  10630  seq3id2  10635  seqhomog  10639  expcl2lemap  10660  nn0ltexp2  10818  facdiv  10847  facwordi  10849  zfz1isolem1  10949  zfz1iso  10950  seq3coll  10951  caucvgre  11163  fimaxre2  11409  climcn1  11490  climcn2  11491  subcn2  11493  summodclem2a  11563  fsumsplitf  11590  fsum2d  11617  modfsummod  11640  fsumabs  11647  telfsumo  11648  fsumiun  11659  prodfdivap  11729  fprod2d  11805  fproddivapf  11813  fprodsplitf  11814  fprodsplit1f  11816  ndvdssub  12112  bezoutlemmain  12190  bezoutlemex  12193  bezoutlemzz  12194  bezoutlemsup  12201  dfgcd2  12206  algcvg  12241  algcvga  12244  algfx  12245  lcmgcdlem  12270  lcmdvds  12272  coprmgcdb  12281  coprmdvds1  12284  coprmdvds2  12286  prmind2  12313  dvdsprime  12315  nprm  12316  dvdsprm  12330  exprmfct  12331  isprm5lem  12334  coprm  12337  isprm6  12340  prmfac1  12345  sqrt2irr  12355  pcqmul  12497  pcqcl  12500  pc2dvds  12524  pcz  12526  prmpwdvds  12549  ennnfonelemim  12666  exmidunben  12668  infpn2  12698  setscomd  12744  mhmlem  13320  isnsg2  13409  ghmf1  13479  islring  13824  lringuplu  13828  rrgval  13894  rrgeq0i  13896  isdomn  13901  domneq0  13904  opprdomnbg  13906  znidom  14289  znrrg  14292  uniopn  14321  fiinopn  14324  epttop  14410  cnpval  14518  iscnp  14519  icnpimaex  14531  lmcvg  14537  cnptoprest  14559  cnptoprest2  14560  lmss  14566  lmff  14569  txcnp  14591  txlm  14599  cnmpt12  14607  cnmpt22  14614  blssps  14747  blss  14748  metss  14814  comet  14819  metcnp3  14831  metcnp2  14833  txmetcnp  14838  divcnap  14885  mpomulcn  14886  elcncf2  14894  cncfi  14898  mulc1cncf  14909  cncfmet  14912  mulcncflem  14927  mulcncf  14928  dedekindeulemloc  14939  dedekindeulemlu  14941  dedekindeulemeu  14942  suplociccreex  14944  dedekindicclemloc  14948  dedekindicclemlu  14950  dedekindicclemeu  14951  ivthinclemlopn  14956  ivthinclemlr  14957  ivthinclemuopn  14958  ivthinclemur  14959  ivthinclemloc  14961  ivthreinc  14965  limccl  14979  ellimc3apf  14980  limccnpcntop  14995  limccnp2lem  14996  limccoap  14998  dvcoapbr  15027  dvmptfsum  15045  mpodvdsmulf1o  15310  perfectlem2  15320  lgsdir2lem4  15356  gausslemma2dlem0i  15382  lgseisenlem2  15396  lgsquad2lem2  15407  2sqlem6  15445  2sqlem8  15448  2sqlem10  15450  cbvrald  15518  bj-bdfindes  15679  bj-omtrans  15686  bj-inf2vnlem1  15700  bj-inf2vnlem2  15701  bj-inf2vnlem3  15702  bj-inf2vnlem4  15703  bj-findes  15711  strcoll2  15713  sscoll2  15718  subctctexmid  15731  pw1nct  15734  exmidsbthrlem  15753  sbthom  15757  apdiff  15779  ismkvnnlem  15783  nconstwlpolem  15796  neapmkv  15799  neap0mkv  15800  ltlenmkv  15801