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  6442  addassnq0  6445  elinp  6457  prcdnql  6467  prcunqu  6468  prarloclem3  6480  caucvgpr  6653  ltsosr  6692  pitonn  6744  axpre-ltwlin  6767  nnaddcl  7715  nnmulcl  7716  zaddcllempos  8058  zaddcllemneg  8060  prime  8113  peano5uzti  8122  uzind2  8126  zindd  8132  uzaddcl  8305  frec2uzltd  8870  frec2uzrdg  8876  frecuzrdgfn  8879  iseqfveq2  8905  expivallem  8910  expcllem  8920  expap0  8939  mulexp  8948  expadd  8951  expmul  8954  leexp2r  8962  leexp1a  8963  bernneq  9022  cjexp  9121  bdbm1.3ii  9346  bj-2inf  9397  bj-omtrans  9416