Theorem imbi12d 223

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 220	. 2 ⊢ (φ → ((ψ → θ) ↔ (χ → θ)))
3		imbi12d.2	. . 3 ⊢ (φ → (θ ↔ τ))
4	3	imbi2d 219	. 2 ⊢ (φ → ((χ → θ) ↔ (χ → τ)))
5	2, 4	bitrd 177	1 ⊢ (φ → ((ψ → θ) ↔ (χ → τ)))

Syntax hints:   → wi 4   ↔ wb 98

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101

This theorem depends on definitions:  df-bi 110

This theorem is referenced by:  nfbidf  1429  drnf1  1618  drnf2  1619  equveli  1639  ax11v2  1698  ax11v  1705  ax11ev  1706  equs5or  1708  mobidh  1931  mobid  1932  axext3  2020  cbvralf  2521  cbvraldva2  2531  gencbval  2596  vtoclgaf  2612  vtocl2gaf  2614  vtocl3gaf  2616  rspct  2643  rspc  2644  ceqex  2665  ralab2  2699  mob2  2715  mob  2717  morex  2719  reu7  2730  reu8  2731  nelrdva  2740  cdeqim  2751  sbcimg  2798  csbhypf  2879  cbvralcsf  2902  dfss2f  2930  sbcssg  3324  sneqrg  3524  elintab  3617  intss1  3621  intmin  3626  dfiin2g  3681  trel  3852  trss  3854  bnd2  3917  zfpow  3919  rext  3942  opth  3965  copsexg  3972  poeq1  4027  pocl  4031  swopolem  4033  swopo  4034  soeq1  4043  sowlin  4048  ordelord  4084  reusv3i  4157  ordtriexmid  4210  onsucsssucexmid  4212  onsucelsucexmid  4215  ordsucunielexmid  4216  regexmidlem1  4218  regexmid  4219  elirr  4224  en2lp  4232  ordsoexmid  4240  tfis  4249  tfisi  4253  peano2  4261  findes  4269  nnregexmid  4285  vtoclr  4331  poinxp  4352  soinxp  4353  posng  4355  ssrel  4371  ssrel2  4373  ssrelrel  4383  relop  4429  issref  4650  iota5  4830  dffun4f  4861  sbcfung  4868  funopg  4877  brprcneu  5114  funfveu  5131  tz6.12f  5145  funbrfv  5155  ssimaexg  5178  fvmptss2  5190  fvmptssdm  5198  fvmptf  5206  fvelrn  5241  f1veqaeq  5351  dff13f  5352  isopolem  5404  isosolem  5406  riota5f  5435  oprabid  5480  ovmpt2s  5566  ov2gf  5567  ovi3  5579  caovcan  5607  caovordig  5608  caofrss  5677  caoftrn  5678  dfoprab4f  5761  f1o2ndf1  5791  poxp  5794  smoel  5856  tfrlem1  5864  nnsucelsuc  6009  nnsucsssuc  6010  nnmordi  6025  nnaordex  6036  qsel  6119  eroveu  6133  ecopovtrn  6139  ecopovtrng  6142  th3qlem2  6145  fundmeng  6223  ssfiexmid  6254  ltsonq  6382  ltexnqq  6391  prcdnql  6466  prcunqu  6467  prloc  6473  prdisj  6474  genprndl  6504  genprndu  6505  lttrsr  6650  ltsosr  6652  recexgt0sr  6661  mulgt0sr  6664  aptisr  6665  mulextsr1  6667  axprecex  6724  axpre-ltwlin  6727  axpre-lttrn  6728  axpre-apti  6729  axpre-mulgt0  6731  axpre-mulext  6732  ltleletr  6857  squeeze0  7611  nnsub  7693  fzind  8089  uzind4s  8269  uzind4s2  8270  indstr  8272  frec2uzzd  8827  frec2uzuzd  8829  frec2uzltd  8830  iseqfveq2  8865  expcl2lemap  8881  cbvrald  9196  bj-bdfindes  9337  bj-omtrans  9344  bj-inf2vnlem1  9354  bj-inf2vnlem2  9355  bj-inf2vnlem3  9356  bj-inf2vnlem4  9357  bj-findes  9365  strcoll2  9367  sscoll2  9372