Theorem imbi2d 230

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 105

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This proof depends on definitions:  df-bi 117

This theorem is used by:  imbi12d  234  imbi2  237  pm5.42  320  imanst  900  pm4.14dc  902  imimorbdc  908  pm5.6dc  938  ax11v2  1873  ax11v  1880  equs5or  1883  mo23  2128  nfabdw  2411  2gencl  2855  3gencl  2856  vtocl2gf  2885  vtocl3gf  2886  vtocl4g  2894  vtocl4ga  2895  eqeu  2996  mo2icl  3005  euind  3013  reu7  3021  reuind  3031  sbctt  3118  reu8nf  3133  sbcnestgf  3199  preq12bg  3898  elint  3976  elintrabg  3983  intab  3999  trss  4238  bm1.3ii  4254  pocl  4448  swopolem  4450  sowlin  4465  frforeq3  4492  frirrg  4495  frind  4497  reusv3  4606  regexmid  4682  ordsoexmid  4709  tfisi  4734  finds2  4748  nnregexmid  4768  vtoclr  4823  2optocl  4852  3optocl  4853  raliunxp  4921  resieq  5073  iss  5109  cnveqb  5243  iotaexab  5356  funmo  5392  fnbrfvb  5741  fvelimab  5759  fvmptssdm  5790  fmptco  5874  fnressn  5901  fressnfv  5902  isoselem  6026  isosolem  6030  ovg  6228  caovcan  6254  caovordig  6255  caovord  6261  f1o2ndf1  6464  poxp  6468  smoeq  6561  smores  6563  tfrlem1  6579  tfrlemi1  6603  tfrexlem  6605  tfri3  6638  oawordriexmid  6743  nnacl  6753  nnmcl  6754  nnacom  6757  nnaass  6758  nndi  6759  nnmass  6760  nnmsucr  6761  nnmcom  6762  nnsucsssuc  6765  nntri3or  6766  nnaordi  6781  nnaword  6784  nnmordi  6789  nnaordex  6801  2ecoptocl  6897  3ecoptocl  6898  th3qlem2  6912  xpdom2g  7130  findcard2  7193  findcard2s  7194  xpfi  7239  supeq1  7327  ordiso2  7376  updjud  7423  nnnninfeq  7469  exmidontriimlem4  7581  exmidontriim  7582  papcotr  7614  distrnq0  7827  addassnq0  7830  elinp  7842  prcdnql  7852  prcunqu  7853  prarloclem3  7865  caucvgpr  8050  caucvgprpr  8080  ltsosr  8132  caucvgsrlemcau  8161  caucvgsrlemgt1  8163  caucvgsrlemoffres  8168  pitonn  8216  axpre-ltwlin  8251  axcaucvglemres  8267  sup3exmid  9290  nnaddcl  9327  nnmulcl  9328  zaddcllempos  9686  zaddcllemneg  9688  prime  9750  peano5uzti  9759  uzind2  9763  zindd  9769  uzaddcl  9996  exfzdc  10670  infssuzex  10677  nninfdcex  10683  frec2uzltd  10854  frec2uzrdg  10860  frecuzrdgtcl  10863  frecuzrdgg  10867  frecuzrdgfunlem  10870  seq3val  10911  seqvalcd  10912  seq3clss  10922  seq3fveq2  10926  seqfveq2g  10928  seq3shft2  10932  seqshft2g  10933  monoord  10936  seq3split  10939  seqsplitg  10940  seq3caopr3  10942  seqcaopr3g  10943  seq3f1olemp  10966  seqf1oglem2a  10969  seqf1og  10972  seq3id3  10975  seq3id2  10977  seq3homo  10978  seq3z  10979  seqhomog  10981  seqfeq4g  10982  ser3ge0  10987  exp3vallem  10991  expcllem  11001  expap0  11020  mulexp  11029  expadd  11032  expmul  11035  leexp2r  11044  leexp1a  11045  bernneq  11112  modqexp  11118  nn0ltexp2  11162  apexp1  11171  facdiv  11191  faclbnd  11194  faclbnd6  11197  omgadd  11257  hashmap  11283  hashf1  11302  seq3coll  11309  wrdind  11509  wrd2ind  11510  pfxccatin12lem3  11519  shftvalg  11616  shftval4g  11617  cjexp  11673  resqrexlemover  11791  resqrexlemdecn  11793  resqrexlemlo  11794  resqrexlemcalc3  11797  absexp  11861  climshft  12088  climub  12128  climserle  12129  fsum2d  12220  fsumabs  12250  fsumiun  12262  binom  12269  bcxmas  12274  cvgratnnlemnexp  12309  cvgratnnlemmn  12310  clim2prod  12324  prodfap0  12330  prodfrecap  12331  fprodabs  12401  fprod2d  12408  demoivreALT  12559  dvdsfac  12645  bitsinv1  12747  bezoutlemstep  12792  bezoutlemmain  12793  bezoutlemex  12796  dfgcd2  12809  gcdmultiple  12815  rplpwr  12822  nn0seqcvgd  12837  alginv  12843  algcvga  12847  algfx  12848  isprm4  12915  prmind2  12916  prmdvdsexp  12945  prmfac1  12949  eulerthlemrprm  13029  eulerthlema  13030  reumodprminv  13054  pcmpt  13144  pcfac  13151  prmpwdvds  13156  prmlem1a  13243  ennnfoneleminc  13353  ennnfonelemkh  13354  ennnfonelemhf1o  13355  ennnfonelemhom  13357  nninfdclemlt  13393  mulgnnass  14011  mhmmulg  14017  gzsumconst  14194  srgmulgass  14344  srgpcomp  14345  lmodvsmmulgdi  14711  cnfldexp  14965  assamulgscm  15094  mplelbascoe  15135  fiinopn  15157  cnpfval  15348  iscnp3  15356  cnprcl2k  15359  tgcn  15361  lmbr  15366  lmbr2  15367  lmbrf  15368  lmss  15399  cnmptcom  15451  metss  15647  metcnp  15665  metcnpi  15668  metcnpi2  15669  elcncf  15726  cncfi  15731  rescncf  15734  cncfco  15744  cdivcncfap  15757  ellimc3apf  15813  limcdifap  15815  limcmpted  15816  limcimo  15818  limcresi  15819  cnplimclemr  15822  limccoap  15831  dvmptfsum  15878  plycolemc  15911  rpcxpmul2  16071  perfectlem2  16222  bcmono  16226  bposlem5  16237  lgsquad2lem2  16323  eupth2fi  16842  depindlem2  16870  depindlem3  16871  bdbm1.3ii  17039  bj-2inf  17086  bj-omtrans  17104  exmidcon  17159  exmidpeirce  17160  wexmiddiffilem  17165  nninfalllem1  17173  nninfsellemdc  17175  nninfsellemqall  17180