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  3534  elint  3611  elintrabg  3618  intab  3634  trss  3853  bm1.3ii  3868  pocl  4030  swopolem  4032  sowlin  4047  reusv3  4157  regexmid  4218  ordsoexmid  4239  tfisi  4252  finds2  4266  nnregexmid  4284  vtoclr  4330  2optocl  4359  3optocl  4360  raliunxp  4419  resieq  4564  iss  4596  cnveqb  4718  funmo  4858  fnbrfvb  5155  fvelimab  5170  fvmptssdm  5196  fmptco  5271  fnressn  5290  fressnfv  5291  isoselem  5400  isosolem  5404  ovg  5578  caovcan  5604  caovordig  5605  caovord  5611  f1o2ndf1  5788  poxp  5791  smoeq  5843  smores  5845  tfrlem1  5861  tfrlemi1  5884  tfrexlem  5886  tfri3  5891  rdgon  5910  nnacl  5991  nnmcl  5992  nnacom  5995  nnaass  5996  nndi  5997  nnmass  5998  nnmsucr  5999  nnmcom  6000  nnsucsssuc  6003  nntri3or  6004  nnaordi  6010  nnaword  6013  nnmordi  6018  nnaordex  6029  2ecoptocl  6123  3ecoptocl  6124  th3qlem2  6138  xpdom2g  6235  distrnq0  6434  addassnq0  6437  elinp  6449  prcdnql  6459  prcunqu  6460  prarloclem3  6472  ltsosr  6644  pitonn  6696  axpre-ltwlin  6719  nnaddcl  7666  nnmulcl  7667  zaddcllempos  8008  zaddcllemneg  8010  prime  8062  peano5uzti  8071  uzind2  8075  zindd  8081  uzaddcl  8254  frec2uzltd  8816  bdbm1.3ii  8944  bj-2inf  8991  bj-omtrans  9009