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  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  3896  elint  3974  elintrabg  3981  intab  3997  trss  4236  bm1.3ii  4252  pocl  4446  swopolem  4448  sowlin  4463  frforeq3  4490  frirrg  4493  frind  4495  reusv3  4604  regexmid  4680  ordsoexmid  4707  tfisi  4732  finds2  4746  nnregexmid  4766  vtoclr  4821  2optocl  4850  3optocl  4851  raliunxp  4919  resieq  5071  iss  5107  cnveqb  5241  iotaexab  5354  funmo  5390  fnbrfvb  5738  fvelimab  5756  fvmptssdm  5787  fmptco  5868  fnressn  5895  fressnfv  5896  isoselem  6020  isosolem  6024  ovg  6222  caovcan  6248  caovordig  6249  caovord  6255  f1o2ndf1  6458  poxp  6462  smoeq  6555  smores  6557  tfrlem1  6573  tfrlemi1  6597  tfrexlem  6599  tfri3  6632  oawordriexmid  6737  nnacl  6747  nnmcl  6748  nnacom  6751  nnaass  6752  nndi  6753  nnmass  6754  nnmsucr  6755  nnmcom  6756  nnsucsssuc  6759  nntri3or  6760  nnaordi  6775  nnaword  6778  nnmordi  6783  nnaordex  6795  2ecoptocl  6891  3ecoptocl  6892  th3qlem2  6906  xpdom2g  7124  findcard2  7187  findcard2s  7188  xpfi  7233  supeq1  7320  ordiso2  7369  updjud  7416  nnnninfeq  7462  exmidontriimlem4  7574  exmidontriim  7575  papcotr  7607  distrnq0  7820  addassnq0  7823  elinp  7835  prcdnql  7845  prcunqu  7846  prarloclem3  7858  caucvgpr  8043  caucvgprpr  8073  ltsosr  8125  caucvgsrlemcau  8154  caucvgsrlemgt1  8156  caucvgsrlemoffres  8161  pitonn  8209  axpre-ltwlin  8244  axcaucvglemres  8260  sup3exmid  9281  nnaddcl  9307  nnmulcl  9308  zaddcllempos  9664  zaddcllemneg  9666  prime  9728  peano5uzti  9737  uzind2  9741  zindd  9747  uzaddcl  9969  exfzdc  10642  infssuzex  10649  nninfdcex  10655  frec2uzltd  10823  frec2uzrdg  10829  frecuzrdgtcl  10832  frecuzrdgg  10836  frecuzrdgfunlem  10839  seq3val  10880  seqvalcd  10881  seq3clss  10891  seq3fveq2  10895  seqfveq2g  10897  seq3shft2  10901  seqshft2g  10902  monoord  10905  seq3split  10908  seqsplitg  10909  seq3caopr3  10911  seqcaopr3g  10912  seq3f1olemp  10935  seqf1oglem2a  10938  seqf1og  10941  seq3id3  10944  seq3id2  10946  seq3homo  10947  seq3z  10948  seqhomog  10950  seqfeq4g  10951  ser3ge0  10956  exp3vallem  10960  expcllem  10970  expap0  10989  mulexp  10998  expadd  11001  expmul  11004  leexp2r  11013  leexp1a  11014  bernneq  11081  modqexp  11087  nn0ltexp2  11130  apexp1  11139  facdiv  11159  faclbnd  11162  faclbnd6  11165  omgadd  11225  hashmap  11251  hashf1  11270  seq3coll  11277  wrdind  11477  wrd2ind  11478  pfxccatin12lem3  11487  shftvalg  11584  shftval4g  11585  cjexp  11641  resqrexlemover  11759  resqrexlemdecn  11761  resqrexlemlo  11762  resqrexlemcalc3  11765  absexp  11828  climshft  12053  climub  12093  climserle  12094  fsum2d  12185  fsumabs  12215  fsumiun  12227  binom  12234  bcxmas  12239  cvgratnnlemnexp  12274  cvgratnnlemmn  12275  clim2prod  12289  prodfap0  12295  prodfrecap  12296  fprodabs  12366  fprod2d  12373  demoivreALT  12524  dvdsfac  12610  bitsinv1  12712  bezoutlemstep  12757  bezoutlemmain  12758  bezoutlemex  12761  dfgcd2  12774  gcdmultiple  12780  rplpwr  12787  nn0seqcvgd  12802  alginv  12808  algcvga  12812  algfx  12813  isprm4  12880  prmind2  12881  prmdvdsexp  12909  prmfac1  12913  eulerthlemrprm  12990  eulerthlema  12991  reumodprminv  13015  pcmpt  13105  pcfac  13112  prmpwdvds  13117  ennnfoneleminc  13285  ennnfonelemkh  13286  ennnfonelemhf1o  13287  ennnfonelemhom  13289  nninfdclemlt  13325  mulgnnass  13943  mhmmulg  13949  gzsumconst  14126  srgmulgass  14276  srgpcomp  14277  lmodvsmmulgdi  14643  cnfldexp  14897  assamulgscm  15026  mplelbascoe  15066  fiinopn  15088  cnpfval  15279  iscnp3  15287  cnprcl2k  15290  tgcn  15292  lmbr  15297  lmbr2  15298  lmbrf  15299  lmss  15330  cnmptcom  15382  metss  15578  metcnp  15596  metcnpi  15599  metcnpi2  15600  elcncf  15657  cncfi  15662  rescncf  15665  cncfco  15675  cdivcncfap  15688  ellimc3apf  15744  limcdifap  15746  limcmpted  15747  limcimo  15749  limcresi  15750  cnplimclemr  15753  limccoap  15762  dvmptfsum  15809  plycolemc  15842  rpcxpmul2  15998  perfectlem2  16097  lgsquad2lem2  16184  eupth2fi  16703  depindlem2  16731  depindlem3  16732  bdbm1.3ii  16900  bj-2inf  16947  bj-omtrans  16965  exmidcon  17019  exmidpeirce  17020  nninfalllem1  17025  nninfsellemdc  17027  nninfsellemqall  17032