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  888  pm4.14dc  890  imimorbdc  896  pm5.6dc  926  ax11v2  1820  ax11v  1827  equs5or  1830  mo23  2067  nfabdw  2338  2gencl  2772  3gencl  2773  vtocl2gf  2801  vtocl3gf  2802  eqeu  2909  mo2icl  2918  euind  2926  reu7  2934  reuind  2944  sbctt  3031  sbcnestgf  3110  preq12bg  3775  elint  3852  elintrabg  3859  intab  3875  trss  4112  bm1.3ii  4126  pocl  4305  swopolem  4307  sowlin  4322  frforeq3  4349  frirrg  4352  frind  4354  reusv3  4462  regexmid  4536  ordsoexmid  4563  tfisi  4588  finds2  4602  nnregexmid  4622  vtoclr  4676  2optocl  4705  3optocl  4706  raliunxp  4770  resieq  4919  iss  4955  cnveqb  5086  funmo  5233  fnbrfvb  5558  fvelimab  5574  fvmptssdm  5602  fmptco  5684  fnressn  5704  fressnfv  5705  isoselem  5823  isosolem  5827  ovg  6015  caovcan  6041  caovordig  6042  caovord  6048  f1o2ndf1  6231  poxp  6235  smoeq  6293  smores  6295  tfrlem1  6311  tfrlemi1  6335  tfrexlem  6337  tfri3  6370  oawordriexmid  6473  nnacl  6483  nnmcl  6484  nnacom  6487  nnaass  6488  nndi  6489  nnmass  6490  nnmsucr  6491  nnmcom  6492  nnsucsssuc  6495  nntri3or  6496  nnaordi  6511  nnaword  6514  nnmordi  6519  nnaordex  6531  2ecoptocl  6625  3ecoptocl  6626  th3qlem2  6640  xpdom2g  6834  findcard2  6891  findcard2s  6892  xpfi  6931  supeq1  6987  ordiso2  7036  updjud  7083  nnnninfeq  7128  exmidontriimlem4  7225  exmidontriim  7226  distrnq0  7460  addassnq0  7463  elinp  7475  prcdnql  7485  prcunqu  7486  prarloclem3  7498  caucvgpr  7683  caucvgprpr  7713  ltsosr  7765  caucvgsrlemcau  7794  caucvgsrlemgt1  7796  caucvgsrlemoffres  7801  pitonn  7849  axpre-ltwlin  7884  axcaucvglemres  7900  sup3exmid  8916  nnaddcl  8941  nnmulcl  8942  zaddcllempos  9292  zaddcllemneg  9294  prime  9354  peano5uzti  9363  uzind2  9367  zindd  9373  uzaddcl  9588  exfzdc  10242  frec2uzltd  10405  frec2uzrdg  10411  frecuzrdgtcl  10414  frecuzrdgg  10418  frecuzrdgfunlem  10421  seq3val  10460  seqvalcd  10461  seq3clss  10469  seq3fveq2  10471  seq3shft2  10475  monoord  10478  seq3split  10481  seq3caopr3  10483  seq3f1olemp  10504  seq3id3  10509  seq3id2  10511  seq3homo  10512  seq3z  10513  ser3ge0  10519  exp3vallem  10523  expcllem  10533  expap0  10552  mulexp  10561  expadd  10564  expmul  10567  leexp2r  10576  leexp1a  10577  bernneq  10643  modqexp  10649  nn0ltexp2  10691  apexp1  10700  facdiv  10720  faclbnd  10723  faclbnd6  10726  omgadd  10784  seq3coll  10824  shftvalg  10847  shftval4g  10848  cjexp  10904  resqrexlemover  11021  resqrexlemdecn  11023  resqrexlemlo  11024  resqrexlemcalc3  11027  absexp  11090  climshft  11314  climub  11354  climserle  11355  fsum2d  11445  fsumabs  11475  fsumiun  11487  binom  11494  bcxmas  11499  cvgratnnlemnexp  11534  cvgratnnlemmn  11535  clim2prod  11549  prodfap0  11555  prodfrecap  11556  fprodabs  11626  fprod2d  11633  demoivreALT  11783  dvdsfac  11868  infssuzex  11952  nninfdcex  11956  bezoutlemstep  12000  bezoutlemmain  12001  bezoutlemex  12004  dfgcd2  12017  gcdmultiple  12023  rplpwr  12030  nn0seqcvgd  12043  alginv  12049  algcvga  12053  algfx  12054  isprm4  12121  prmind2  12122  prmdvdsexp  12150  prmfac1  12154  eulerthlemrprm  12231  eulerthlema  12232  reumodprminv  12255  pcmpt  12343  pcfac  12350  prmpwdvds  12355  ennnfoneleminc  12414  ennnfonelemkh  12415  ennnfonelemhf1o  12416  ennnfonelemhom  12418  nninfdclemlt  12454  mulgnnass  13023  mhmmulg  13029  srgmulgass  13177  srgpcomp  13178  lmodvsmmulgdi  13418  cnfldexp  13556  fiinopn  13589  cnpfval  13780  iscnp3  13788  cnprcl2k  13791  tgcn  13793  lmbr  13798  lmbr2  13799  lmbrf  13800  lmss  13831  cnmptcom  13883  metss  14079  metcnp  14097  metcnpi  14100  metcnpi2  14101  elcncf  14145  cncfi  14150  rescncf  14153  cncfco  14163  cdivcncfap  14172  ellimc3apf  14214  limcdifap  14216  limcmpted  14217  limcimo  14219  limcresi  14220  cnplimclemr  14223  limccoap  14232  bdbm1.3ii  14728  bj-2inf  14775  bj-omtrans  14793  nninfalllem1  14842  nninfsellemdc  14844  nninfsellemqall  14849