Theorem imbi2d 228

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 180	1 ⊢ (𝜑 → ((𝜃 → 𝜓) ↔ (𝜃 → 𝜒)))

Syntax hints:   → wi 4   ↔ wb 103

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106

This theorem depends on definitions:  df-bi 115

This theorem is referenced by:  imbi12d  232  imbi2  235  pm5.42  313  imandc  819  pm4.14dc  820  imimorbdc  828  pm5.6dc  868  ax11v2  1741  ax11v  1748  equs5or  1751  mo23  1982  2gencl  2632  3gencl  2633  vtocl2gf  2660  vtocl3gf  2661  eqeu  2762  mo2icl  2771  euind  2779  reu7  2787  reuind  2795  sbctt  2880  sbcnestgf  2953  preq12bg  3565  elint  3642  elintrabg  3649  intab  3665  trss  3884  bm1.3ii  3899  pocl  4058  swopolem  4060  sowlin  4075  frforeq3  4102  frirrg  4105  frind  4107  reusv3  4210  regexmid  4278  ordsoexmid  4305  tfisi  4328  finds2  4342  nnregexmid  4360  vtoclr  4406  2optocl  4435  3optocl  4436  raliunxp  4495  resieq  4640  iss  4674  cnveqb  4796  funmo  4937  fnbrfvb  5235  fvelimab  5250  fvmptssdm  5276  fmptco  5351  fnressn  5370  fressnfv  5371  isoselem  5479  isosolem  5483  ovg  5659  caovcan  5685  caovordig  5686  caovord  5692  f1o2ndf1  5869  poxp  5873  smoeq  5928  smores  5930  tfrlem1  5946  tfrlemi1  5969  tfrexlem  5971  tfri3  5976  rdgon  5996  freccl  6016  nnacl  6082  nnmcl  6083  nnacom  6086  nnaass  6087  nndi  6088  nnmass  6089  nnmsucr  6090  nnmcom  6091  nnsucsssuc  6094  nntri3or  6095  nnaordi  6104  nnaword  6107  nnmordi  6112  nnaordex  6123  2ecoptocl  6217  3ecoptocl  6218  th3qlem2  6232  xpdom2g  6329  findcard2  6373  findcard2s  6374  supeq1  6399  ordiso2  6446  distrnq0  6649  addassnq0  6652  elinp  6664  prcdnql  6674  prcunqu  6675  prarloclem3  6687  caucvgpr  6872  caucvgprpr  6902  ltsosr  6941  caucvgsrlemcau  6969  caucvgsrlemgt1  6971  caucvgsrlemoffres  6976  pitonn  7016  axpre-ltwlin  7049  axcaucvglemres  7065  nnaddcl  8059  nnmulcl  8060  zaddcllempos  8388  zaddcllemneg  8390  prime  8446  peano5uzti  8455  uzind2  8459  zindd  8465  uzaddcl  8674  exfzdc  9249  frec2uzltd  9405  frec2uzrdg  9411  frecuzrdgfn  9414  iseqss  9446  iseqfveq2  9448  iseqshft2  9452  monoord  9455  iseqsplit  9458  iseqcaopr3  9460  iseqid3s  9466  iseqhomo  9468  iseqz  9469  expivallem  9477  expcllem  9487  expap0  9506  mulexp  9515  expadd  9518  expmul  9521  leexp2r  9530  leexp1a  9531  bernneq  9593  facdiv  9665  faclbnd  9668  faclbnd6  9671  shftvalg  9724  shftval4g  9725  cjexp  9780  resqrexlemover  9896  resqrexlemdecn  9898  resqrexlemlo  9899  resqrexlemcalc3  9902  absexp  9965  climshft  10143  climub  10182  climserile  10183  dvdsfac  10260  infssuzex  10345  bezoutlemstep  10386  bezoutlemmain  10387  bezoutlemex  10390  dfgcd2  10403  gcdmultiple  10409  rplpwr  10416  nn0seqcvgd  10423  ialginv  10429  ialgcvga  10433  ialgfx  10434  isprm4  10501  prmind2  10502  prmdvdsexp  10527  prmfac1  10531  bdbm1.3ii  10682  bj-2inf  10733  bj-omtrans  10751