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  9251  nnaddcl  9277  nnmulcl  9278  zaddcllempos  9634  zaddcllemneg  9636  prime  9698  peano5uzti  9707  uzind2  9711  zindd  9717  uzaddcl  9939  exfzdc  10611  infssuzex  10618  nninfdcex  10624  frec2uzltd  10792  frec2uzrdg  10798  frecuzrdgtcl  10801  frecuzrdgg  10805  frecuzrdgfunlem  10808  seq3val  10849  seqvalcd  10850  seq3clss  10860  seq3fveq2  10864  seqfveq2g  10866  seq3shft2  10870  seqshft2g  10871  monoord  10874  seq3split  10877  seqsplitg  10878  seq3caopr3  10880  seqcaopr3g  10881  seq3f1olemp  10904  seqf1oglem2a  10907  seqf1og  10910  seq3id3  10913  seq3id2  10915  seq3homo  10916  seq3z  10917  seqhomog  10919  seqfeq4g  10920  ser3ge0  10925  exp3vallem  10929  expcllem  10939  expap0  10958  mulexp  10967  expadd  10970  expmul  10973  leexp2r  10982  leexp1a  10983  bernneq  11050  modqexp  11056  nn0ltexp2  11099  apexp1  11108  facdiv  11128  faclbnd  11131  faclbnd6  11134  omgadd  11194  hashmap  11220  seq3coll  11242  wrdind  11442  wrd2ind  11443  pfxccatin12lem3  11452  shftvalg  11549  shftval4g  11550  cjexp  11606  resqrexlemover  11724  resqrexlemdecn  11726  resqrexlemlo  11727  resqrexlemcalc3  11730  absexp  11793  climshft  12018  climub  12058  climserle  12059  fsum2d  12150  fsumabs  12180  fsumiun  12192  binom  12199  bcxmas  12204  cvgratnnlemnexp  12239  cvgratnnlemmn  12240  clim2prod  12254  prodfap0  12260  prodfrecap  12261  fprodabs  12331  fprod2d  12338  demoivreALT  12489  dvdsfac  12575  bitsinv1  12677  bezoutlemstep  12722  bezoutlemmain  12723  bezoutlemex  12726  dfgcd2  12739  gcdmultiple  12745  rplpwr  12752  nn0seqcvgd  12767  alginv  12773  algcvga  12777  algfx  12778  isprm4  12845  prmind2  12846  prmdvdsexp  12874  prmfac1  12878  eulerthlemrprm  12955  eulerthlema  12956  reumodprminv  12980  pcmpt  13070  pcfac  13077  prmpwdvds  13082  ennnfoneleminc  13250  ennnfonelemkh  13251  ennnfonelemhf1o  13252  ennnfonelemhom  13254  nninfdclemlt  13290  gsumfzz  13754  mulgnnass  13914  mhmmulg  13920  gsumfzconst  14098  srgmulgass  14236  srgpcomp  14237  lmodvsmmulgdi  14601  cnfldexp  14855  gsumfzfsumlemm  14865  mplelbascoe  14977  fiinopn  14999  cnpfval  15190  iscnp3  15198  cnprcl2k  15201  tgcn  15203  lmbr  15208  lmbr2  15209  lmbrf  15210  lmss  15241  cnmptcom  15293  metss  15489  metcnp  15507  metcnpi  15510  metcnpi2  15511  elcncf  15568  cncfi  15573  rescncf  15576  cncfco  15586  cdivcncfap  15599  ellimc3apf  15655  limcdifap  15657  limcmpted  15658  limcimo  15660  limcresi  15661  cnplimclemr  15664  limccoap  15673  dvmptfsum  15720  plycolemc  15753  rpcxpmul2  15908  perfectlem2  15998  lgsquad2lem2  16085  eupth2fi  16604  depindlem2  16632  depindlem3  16633  bdbm1.3ii  16801  bj-2inf  16848  bj-omtrans  16866  exmidcon  16920  exmidpeirce  16921  nninfalllem1  16926  nninfsellemdc  16928  nninfsellemqall  16933