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  6652  pitonn  6704  axpre-ltwlin  6727  nnaddcl  7675  nnmulcl  7676  zaddcllempos  8018  zaddcllemneg  8020  prime  8073  peano5uzti  8082  uzind2  8086  zindd  8092  uzaddcl  8265  frec2uzltd  8830  frec2uzrdg  8836  frecuzrdgfn  8839  iseqfveq2  8865  expivallem  8870  expcllem  8880  expap0  8899  mulexp  8908  expadd  8911  expmul  8914  leexp2r  8922  leexp1a  8923  bernneq  8982  cjexp  9081  bdbm1.3ii  9279  bj-2inf  9326  bj-omtrans  9344