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  785  pm4.14dc  786  imimorbdc  794  pm5.6dc  834  ax11v2  1698  ax11v  1705  equs5or  1708  mo23  1938  2gencl  2581  3gencl  2582  vtocl2gf  2609  vtocl3gf  2610  eqeu  2705  mo2icl  2714  euind  2722  reu7  2730  reuind  2738  sbctt  2818  sbcnestgf  2891  preq12bg  3535  elint  3612  elintrabg  3619  intab  3635  trss  3854  bm1.3ii  3869  pocl  4031  swopolem  4033  sowlin  4048  reusv3  4158  regexmid  4219  ordsoexmid  4240  tfisi  4253  finds2  4267  nnregexmid  4285  vtoclr  4331  2optocl  4360  3optocl  4361  raliunxp  4420  resieq  4565  iss  4597  cnveqb  4719  funmo  4860  fnbrfvb  5157  fvelimab  5172  fvmptssdm  5198  fmptco  5273  fnressn  5292  fressnfv  5293  isoselem  5402  isosolem  5406  ovg  5581  caovcan  5607  caovordig  5608  caovord  5614  f1o2ndf1  5791  poxp  5794  smoeq  5846  smores  5848  tfrlem1  5864  tfrlemi1  5887  tfrexlem  5889  tfri3  5894  rdgon  5913  freccl  5932  nnacl  5998  nnmcl  5999  nnacom  6002  nnaass  6003  nndi  6004  nnmass  6005  nnmsucr  6006  nnmcom  6007  nnsucsssuc  6010  nntri3or  6011  nnaordi  6017  nnaword  6020  nnmordi  6025  nnaordex  6036  2ecoptocl  6130  3ecoptocl  6131  th3qlem2  6145  xpdom2g  6242  distrnq0  6441  addassnq0  6444  elinp  6456  prcdnql  6466  prcunqu  6467  prarloclem3  6479  ltsosr  6672  pitonn  6724  axpre-ltwlin  6747  nnaddcl  7695  nnmulcl  7696  zaddcllempos  8038  zaddcllemneg  8040  prime  8093  peano5uzti  8102  uzind2  8106  zindd  8112  uzaddcl  8285  frec2uzltd  8850  frec2uzrdg  8856  frecuzrdgfn  8859  iseqfveq2  8885  expivallem  8890  expcllem  8900  expap0  8919  mulexp  8928  expadd  8931  expmul  8934  leexp2r  8942  leexp1a  8943  bernneq  9002  cjexp  9101  bdbm1.3ii  9325  bj-2inf  9372  bj-omtrans  9390