Theorem imbi2d 219

Description: Deduction adding an antecedent to both sides of a logical equivalence. (Contributed by NM, 5-Aug-1993.)

Hypothesis

Ref	Expression
imbid.1	⊢ (φ → (ψ ↔ χ))

Assertion

Ref	Expression
imbi2d	⊢ (φ → ((θ → ψ) ↔ (θ → χ)))

Proof of Theorem imbi2d

Step	Hyp	Ref	Expression
1		imbid.1	. . 3 ⊢ (φ → (ψ ↔ χ))
2	1	a1d 22	. 2 ⊢ (φ → (θ → (ψ ↔ χ)))
3	2	pm5.74d 171	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:  imbi12d  223  imbi2  226  pm5.42  303  imandc  779  pm4.14dc  780  imimorbdc  788  pm5.6dc  823  ax11v2  1683  ax11v  1690  equs5or  1693  mo23  1923  2gencl  2564  3gencl  2565  vtocl2gf  2592  vtocl3gf  2593  eqeu  2688  mo2icl  2697  euind  2705  reu7  2713  reuind  2721  sbctt  2801  sbcnestgf  2874  preq12bg  3518  elint  3595  elintrabg  3602  intab  3618  trss  3837  bm1.3ii  3852  pocl  4014  swopolem  4016  sowlin  4031  reusv3  4142  regexmid  4203  ordsoexmid  4224  tfisi  4237  finds2  4251  nnregexmid  4269  vtoclr  4315  2optocl  4344  3optocl  4345  raliunxp  4404  resieq  4549  iss  4581  cnveqb  4703  funmo  4843  fnbrfvb  5139  fvelimab  5154  fvmptssdm  5180  fmptco  5255  fnressn  5274  fressnfv  5275  isoselem  5384  isosolem  5388  ovg  5562  caovcan  5588  caovordig  5589  caovord  5595  f1o2ndf1  5772  poxp  5775  smoeq  5827  smores  5829  tfrlem1  5845  tfrlemi1  5867  tfrexlem  5870  tfri3  5875  rdgon  5893  nnacl  5974  nnmcl  5975  nnacom  5978  nnaass  5979  nndi  5980  nnmass  5981  nnmsucr  5982  nnmcom  5983  nnsucsssuc  5986  nntri3or  5987  nnaordi  5992  nnaword  5995  nnmordi  6000  nnaordex  6011  2ecoptocl  6105  3ecoptocl  6106  th3qlem2  6120  distrnq0  6314  addassnq0  6317  elinp  6328  prcdnql  6338  prcunqu  6339  prarloclem3  6351  ltsosr  6511  axpre-ltwlin  6577  bdbm1.3ii  7117  bj-2inf  7160  bj-omtrans  7178