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  6467  prcunqu  6468  prloc  6474  prdisj  6475  genprndl  6504  genprndu  6505  caucvgprlemnkj  6637  caucvgprlemnbj  6638  caucvgprlemcl  6647  lttrsr  6690  ltsosr  6692  recexgt0sr  6701  mulgt0sr  6704  aptisr  6705  mulextsr1  6707  axprecex  6764  axpre-ltwlin  6767  axpre-lttrn  6768  axpre-apti  6769  axpre-mulgt0  6771  axpre-mulext  6772  ltleletr  6897  squeeze0  7651  nnsub  7733  fzind  8129  uzind4s  8309  uzind4s2  8310  indstr  8312  frec2uzzd  8867  frec2uzuzd  8869  frec2uzltd  8870  iseqfveq2  8905  expcl2lemap  8921  cbvrald  9262  bj-bdfindes  9409  bj-omtrans  9416  bj-inf2vnlem1  9430  bj-inf2vnlem2  9431  bj-inf2vnlem3  9432  bj-inf2vnlem4  9433  bj-findes  9441  strcoll2  9443  sscoll2  9448