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  1410  drnf1  1599  drnf2  1600  equveli  1620  ax11v2  1679  ax11v  1686  ax11ev  1687  equs5or  1689  mobidh  1912  mobid  1913  axext3  2001  cbvralf  2501  cbvraldva2  2511  gencbval  2575  vtoclgaf  2591  vtocl2gaf  2593  vtocl3gaf  2595  rspct  2622  rspc  2623  ceqex  2644  ralab2  2678  mob2  2694  mob  2696  morex  2698  reu7  2709  reu8  2710  nelrdva  2719  cdeqim  2730  sbcimg  2777  csbhypf  2858  cbvralcsf  2881  dfss2f  2909  sbcssg  3305  sneqrg  3503  elintab  3596  intss1  3600  intmin  3605  dfiin2g  3660  trel  3831  trss  3833  bnd2  3896  zfpow  3898  rext  3921  opth  3944  copsexg  3951  poeq1  4006  pocl  4010  swopolem  4012  swopo  4013  soeq1  4022  sowlin  4027  ordelord  4063  reusv3i  4137  ordtriexmid  4190  onsucsssucexmid  4192  onsucelsucexmid  4195  ordsucunielexmid  4196  regexmidlem1  4198  regexmid  4199  elirr  4204  en2lp  4212  ordsoexmid  4220  tfis  4229  tfisi  4233  peano2  4241  findes  4249  nnregexmid  4265  vtoclr  4311  poinxp  4332  soinxp  4333  posng  4335  ssrel  4351  ssrel2  4353  ssrelrel  4363  relop  4409  issref  4630  iota5  4810  dffun4f  4840  sbcfung  4847  funopg  4856  brprcneu  5092  funfveu  5109  tz6.12f  5123  funbrfv  5133  ssimaexg  5156  fvmptss2  5168  fvmptssdm  5176  fvmptf  5184  fvelrn  5219  f1veqaeq  5329  dff13f  5330  isopolem  5382  isosolem  5384  riota5f  5412  oprabid  5457  ovmpt2s  5543  ov2gf  5544  ovi3  5556  caovcan  5584  caovordig  5585  caofrss  5654  caoftrn  5655  dfoprab4f  5738  f1o2ndf1  5768  poxp  5771  smoel  5833  tfrlem1  5841  nnsucelsuc  5981  nnsucsssuc  5982  nnmordi  5996  nnaordex  6007  qsel  6090  eroveu  6104  ecopovtrn  6110  ecopovtrng  6113  th3qlem2  6116  ltsonq  6251  ltexnqq  6260  prcdnql  6332  prcunqu  6333  prloc  6339  prdisj  6340  genprndl  6370  genprndu  6371  lttrsr  6503  ltsosr  6505  recexsrlem  6514  mulgt0sr  6516  axprecex  6568  axpre-ltwlin  6571  axpre-lttrn  6572  axpre-mulgt0  6574  ltleletr  6692  cbvrald  7173  bj-bdfindes  7310  bj-omtrans  7317  bj-inf2vnlem1  7327  bj-inf2vnlem2  7328  bj-inf2vnlem3  7329  bj-inf2vnlem4  7330  bj-findes  7338  strcoll2  7340  sscoll2  7345