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  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  7101  fisseneq  7104  fidcenumlemrk  7129  fidcenumlemr  7130  isbth  7142  supeq3  7165  supeq123d  7166  supmoti  7168  suplubti  7175  supisolem  7183  cnvinfex  7193  eqinfti  7195  infvalti  7197  ordiso2  7210  nninfninc  7298  nnnninfeq2  7304  isomni  7311  finomni  7315  exmidomni  7317  ctssexmid  7325  ismkv  7328  ismkvnex  7330  mkvprop  7333  fodjumkvlemres  7334  enmkvlem  7336  iswomni  7340  exmidfodomrlemr  7388  exmidfodomrlemrALT  7389  tapeq1  7446  exmidapne  7454  ccfunen  7458  ltsonq  7593  ltexnqq  7603  prcdnql  7679  prcunqu  7680  prloc  7686  prdisj  7687  genprndl  7716  genprndu  7717  caucvgprlemnkj  7861  caucvgprlemnbj  7862  caucvgprlemcl  7871  caucvgprprlemcbv  7882  caucvgprprlemval  7883  suplocexprlemloc  7916  lttrsr  7957  ltsosr  7959  recexgt0sr  7968  mulgt0sr  7973  aptisr  7974  mulextsr1  7976  srpospr  7978  caucvgsrlemgt1  7990  caucvgsrlemoffres  7995  caucvgsr  7997  map2psrprg  8000  suplocsrlemb  8001  axprecex  8075  axpre-ltwlin  8078  axpre-lttrn  8079  axpre-apti  8080  axpre-mulgt0  8082  axpre-mulext  8083  axcaucvglemcau  8093  axcaucvglemres  8094  axpre-suploclemres  8096  axpre-suploc  8097  axsuploc  8227  ltleletr  8236  ltordlem  8637  squeeze0  9059  sup3exmid  9112  nnsub  9157  fzind  9570  uzind4s  9793  uzind4s2  9794  indstr  9796  supinfneg  9798  infsupneg  9799  frec2uzuzd  10632  frec2uzltd  10633  uzsinds  10674  seq3fveq2  10705  seqfveq2g  10707  seq3shft2  10711  seqshft2g  10712  monoord  10715  seq3split  10718  seqsplitg  10719  seqf1oglem2  10750  seqf1og  10751  seq3id2  10756  seqhomog  10760  expcl2lemap  10781  nn0ltexp2  10939  facdiv  10968  facwordi  10970  zfz1isolem1  11070  zfz1iso  11071  seq3coll  11072  wrdind  11262  wrd2ind  11263  swrdccatin1  11265  swrdccat3blem  11279  reuccatpfxs1lem  11286  caucvgre  11500  fimaxre2  11746  climcn1  11827  climcn2  11828  subcn2  11830  summodclem2a  11900  fsumsplitf  11927  fsum2d  11954  modfsummod  11977  fsumabs  11984  telfsumo  11985  fsumiun  11996  prodfdivap  12066  fprod2d  12142  fproddivapf  12150  fprodsplitf  12151  fprodsplit1f  12153  ndvdssub  12449  bezoutlemmain  12527  bezoutlemex  12530  bezoutlemzz  12531  bezoutlemsup  12538  dfgcd2  12543  algcvg  12578  algcvga  12581  algfx  12582  lcmgcdlem  12607  lcmdvds  12609  coprmgcdb  12618  coprmdvds1  12621  coprmdvds2  12623  prmind2  12650  dvdsprime  12652  nprm  12653  dvdsprm  12667  exprmfct  12668  isprm5lem  12671  coprm  12674  isprm6  12677  prmfac1  12682  sqrt2irr  12692  pcqmul  12834  pcqcl  12837  pc2dvds  12861  pcz  12863  prmpwdvds  12886  ennnfonelemim  13003  exmidunben  13005  infpn2  13035  setscomd  13081  mhmlem  13659  isnsg2  13748  ghmf1  13818  islring  14164  lringuplu  14168  rrgval  14234  rrgeq0i  14236  isdomn  14241  domneq0  14244  opprdomnbg  14246  znidom  14629  znrrg  14632  mplvalcoe  14662  mplsubgfilemcl  14671  uniopn  14683  fiinopn  14686  epttop  14772  cnpval  14880  iscnp  14881  icnpimaex  14893  lmcvg  14899  cnptoprest  14921  cnptoprest2  14922  lmss  14928  lmff  14931  txcnp  14953  txlm  14961  cnmpt12  14969  cnmpt22  14976  blssps  15109  blss  15110  metss  15176  comet  15181  metcnp3  15193  metcnp2  15195  txmetcnp  15200  divcnap  15247  mpomulcn  15248  elcncf2  15256  cncfi  15260  mulc1cncf  15271  cncfmet  15274  mulcncflem  15289  mulcncf  15290  dedekindeulemloc  15301  dedekindeulemlu  15303  dedekindeulemeu  15304  suplociccreex  15306  dedekindicclemloc  15310  dedekindicclemlu  15312  dedekindicclemeu  15313  ivthinclemlopn  15318  ivthinclemlr  15319  ivthinclemuopn  15320  ivthinclemur  15321  ivthinclemloc  15323  ivthreinc  15327  limccl  15341  ellimc3apf  15342  limccnpcntop  15357  limccnp2lem  15358  limccoap  15360  dvcoapbr  15389  dvmptfsum  15407  mpodvdsmulf1o  15672  perfectlem2  15682  lgsdir2lem4  15718  gausslemma2dlem0i  15744  lgseisenlem2  15758  lgsquad2lem2  15769  2sqlem6  15807  2sqlem8  15810  2sqlem10  15812  gropd  15856  grstructd2dom  15857  upgredg2vtx  15954  upgredgpr  15955  cbvrald  16176  bj-bdfindes  16336  bj-omtrans  16343  bj-inf2vnlem1  16357  bj-inf2vnlem2  16358  bj-inf2vnlem3  16359  bj-inf2vnlem4  16360  bj-findes  16368  strcoll2  16370  sscoll2  16375  subctctexmid  16395  pw1nct  16398  exmidsbthrlem  16420  sbthom  16424  apdiff  16446  ismkvnnlem  16450  nconstwlpolem  16463  neapmkv  16466  neap0mkv  16467  ltlenmkv  16468