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

Syntax hints:   → wi 4   ↔ wb 105

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

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  imbi12d  234  imbi2  237  pm5.42  320  imanst  896  pm4.14dc  898  imimorbdc  904  pm5.6dc  934  ax11v2  1869  ax11v  1876  equs5or  1879  mo23  2124  nfabdw  2405  2gencl  2849  3gencl  2850  vtocl2gf  2879  vtocl3gf  2880  vtocl4g  2888  vtocl4ga  2889  eqeu  2990  mo2icl  2999  euind  3007  reu7  3015  reuind  3025  sbctt  3112  reu8nf  3127  sbcnestgf  3193  preq12bg  3882  elint  3960  elintrabg  3967  intab  3983  trss  4222  bm1.3ii  4236  pocl  4429  swopolem  4431  sowlin  4446  frforeq3  4473  frirrg  4476  frind  4478  reusv3  4586  regexmid  4662  ordsoexmid  4689  tfisi  4714  finds2  4728  nnregexmid  4748  vtoclr  4803  2optocl  4832  3optocl  4833  raliunxp  4901  resieq  5053  iss  5089  cnveqb  5223  iotaexab  5336  funmo  5372  fnbrfvb  5720  fvelimab  5738  fvmptssdm  5767  fmptco  5848  fnressn  5875  fressnfv  5876  isoselem  5999  isosolem  6003  ovg  6201  caovcan  6227  caovordig  6228  caovord  6234  f1o2ndf1  6437  poxp  6441  smoeq  6534  smores  6536  tfrlem1  6552  tfrlemi1  6576  tfrexlem  6578  tfri3  6611  oawordriexmid  6716  nnacl  6726  nnmcl  6727  nnacom  6730  nnaass  6731  nndi  6732  nnmass  6733  nnmsucr  6734  nnmcom  6735  nnsucsssuc  6738  nntri3or  6739  nnaordi  6754  nnaword  6757  nnmordi  6762  nnaordex  6774  2ecoptocl  6870  3ecoptocl  6871  th3qlem2  6885  xpdom2g  7096  findcard2  7159  findcard2s  7160  xpfi  7205  supeq1  7290  ordiso2  7339  updjud  7386  nnnninfeq  7432  exmidontriimlem4  7544  exmidontriim  7545  papcotr  7577  distrnq0  7790  addassnq0  7793  elinp  7805  prcdnql  7815  prcunqu  7816  prarloclem3  7828  caucvgpr  8013  caucvgprpr  8043  ltsosr  8095  caucvgsrlemcau  8124  caucvgsrlemgt1  8126  caucvgsrlemoffres  8131  pitonn  8179  axpre-ltwlin  8214  axcaucvglemres  8230  sup3exmid  9248  nnaddcl  9274  nnmulcl  9275  zaddcllempos  9631  zaddcllemneg  9633  prime  9695  peano5uzti  9704  uzind2  9708  zindd  9714  uzaddcl  9936  exfzdc  10608  infssuzex  10615  nninfdcex  10621  frec2uzltd  10789  frec2uzrdg  10795  frecuzrdgtcl  10798  frecuzrdgg  10802  frecuzrdgfunlem  10805  seq3val  10846  seqvalcd  10847  seq3clss  10857  seq3fveq2  10861  seqfveq2g  10863  seq3shft2  10867  seqshft2g  10868  monoord  10871  seq3split  10874  seqsplitg  10875  seq3caopr3  10877  seqcaopr3g  10878  seq3f1olemp  10901  seqf1oglem2a  10904  seqf1og  10907  seq3id3  10910  seq3id2  10912  seq3homo  10913  seq3z  10914  seqhomog  10916  seqfeq4g  10917  ser3ge0  10922  exp3vallem  10926  expcllem  10936  expap0  10955  mulexp  10964  expadd  10967  expmul  10970  leexp2r  10979  leexp1a  10980  bernneq  11047  modqexp  11053  nn0ltexp2  11096  apexp1  11105  facdiv  11125  faclbnd  11128  faclbnd6  11131  omgadd  11191  hashmap  11217  seq3coll  11239  wrdind  11439  wrd2ind  11440  pfxccatin12lem3  11449  shftvalg  11546  shftval4g  11547  cjexp  11603  resqrexlemover  11720  resqrexlemdecn  11722  resqrexlemlo  11723  resqrexlemcalc3  11726  absexp  11789  climshft  12014  climub  12054  climserle  12055  fsum2d  12146  fsumabs  12176  fsumiun  12188  binom  12195  bcxmas  12200  cvgratnnlemnexp  12235  cvgratnnlemmn  12236  clim2prod  12250  prodfap0  12256  prodfrecap  12257  fprodabs  12327  fprod2d  12334  demoivreALT  12485  dvdsfac  12571  bitsinv1  12673  bezoutlemstep  12718  bezoutlemmain  12719  bezoutlemex  12722  dfgcd2  12735  gcdmultiple  12741  rplpwr  12748  nn0seqcvgd  12763  alginv  12769  algcvga  12773  algfx  12774  isprm4  12841  prmind2  12842  prmdvdsexp  12870  prmfac1  12874  eulerthlemrprm  12951  eulerthlema  12952  reumodprminv  12976  pcmpt  13066  pcfac  13073  prmpwdvds  13078  ennnfoneleminc  13246  ennnfonelemkh  13247  ennnfonelemhf1o  13248  ennnfonelemhom  13250  nninfdclemlt  13286  gsumfzz  13792  mulgnnass  13958  mhmmulg  13964  gsumfzconst  14142  srgmulgass  14217  srgpcomp  14218  lmodvsmmulgdi  14583  cnfldexp  14837  gsumfzfsumlemm  14847  mplelbascoe  14959  fiinopn  14981  cnpfval  15172  iscnp3  15180  cnprcl2k  15183  tgcn  15185  lmbr  15190  lmbr2  15191  lmbrf  15192  lmss  15223  cnmptcom  15275  metss  15471  metcnp  15489  metcnpi  15492  metcnpi2  15493  elcncf  15550  cncfi  15555  rescncf  15558  cncfco  15568  cdivcncfap  15581  ellimc3apf  15637  limcdifap  15639  limcmpted  15640  limcimo  15642  limcresi  15643  cnplimclemr  15646  limccoap  15655  dvmptfsum  15702  plycolemc  15735  rpcxpmul2  15890  perfectlem2  15980  lgsquad2lem2  16067  eupth2fi  16586  depindlem2  16614  depindlem3  16615  bdbm1.3ii  16773  bj-2inf  16820  bj-omtrans  16838  exmidcon  16892  exmidpeirce  16893  nninfalllem1  16898  nninfsellemdc  16900  nninfsellemqall  16905