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  7326  ordiso2  7375  updjud  7422  nnnninfeq  7468  exmidontriimlem4  7580  exmidontriim  7581  papcotr  7613  distrnq0  7826  addassnq0  7829  elinp  7841  prcdnql  7851  prcunqu  7852  prarloclem3  7864  caucvgpr  8049  caucvgprpr  8079  ltsosr  8131  caucvgsrlemcau  8160  caucvgsrlemgt1  8162  caucvgsrlemoffres  8167  pitonn  8215  axpre-ltwlin  8250  axcaucvglemres  8266  sup3exmid  9288  nnaddcl  9325  nnmulcl  9326  zaddcllempos  9683  zaddcllemneg  9685  prime  9747  peano5uzti  9756  uzind2  9760  zindd  9766  uzaddcl  9988  exfzdc  10661  infssuzex  10668  nninfdcex  10674  frec2uzltd  10842  frec2uzrdg  10848  frecuzrdgtcl  10851  frecuzrdgg  10855  frecuzrdgfunlem  10858  seq3val  10899  seqvalcd  10900  seq3clss  10910  seq3fveq2  10914  seqfveq2g  10916  seq3shft2  10920  seqshft2g  10921  monoord  10924  seq3split  10927  seqsplitg  10928  seq3caopr3  10930  seqcaopr3g  10931  seq3f1olemp  10954  seqf1oglem2a  10957  seqf1og  10960  seq3id3  10963  seq3id2  10965  seq3homo  10966  seq3z  10967  seqhomog  10969  seqfeq4g  10970  ser3ge0  10975  exp3vallem  10979  expcllem  10989  expap0  11008  mulexp  11017  expadd  11020  expmul  11023  leexp2r  11032  leexp1a  11033  bernneq  11100  modqexp  11106  nn0ltexp2  11149  apexp1  11158  facdiv  11178  faclbnd  11181  faclbnd6  11184  omgadd  11244  hashmap  11270  hashf1  11289  seq3coll  11296  wrdind  11496  wrd2ind  11497  pfxccatin12lem3  11506  shftvalg  11603  shftval4g  11604  cjexp  11660  resqrexlemover  11778  resqrexlemdecn  11780  resqrexlemlo  11781  resqrexlemcalc3  11784  absexp  11847  climshft  12072  climub  12112  climserle  12113  fsum2d  12204  fsumabs  12234  fsumiun  12246  binom  12253  bcxmas  12258  cvgratnnlemnexp  12293  cvgratnnlemmn  12294  clim2prod  12308  prodfap0  12314  prodfrecap  12315  fprodabs  12385  fprod2d  12392  demoivreALT  12543  dvdsfac  12629  bitsinv1  12731  bezoutlemstep  12776  bezoutlemmain  12777  bezoutlemex  12780  dfgcd2  12793  gcdmultiple  12799  rplpwr  12806  nn0seqcvgd  12821  alginv  12827  algcvga  12831  algfx  12832  isprm4  12899  prmind2  12900  prmdvdsexp  12928  prmfac1  12932  eulerthlemrprm  13009  eulerthlema  13010  reumodprminv  13034  pcmpt  13124  pcfac  13131  prmpwdvds  13136  ennnfoneleminc  13304  ennnfonelemkh  13305  ennnfonelemhf1o  13306  ennnfonelemhom  13308  nninfdclemlt  13344  mulgnnass  13962  mhmmulg  13968  gzsumconst  14145  srgmulgass  14295  srgpcomp  14296  lmodvsmmulgdi  14662  cnfldexp  14916  assamulgscm  15045  mplelbascoe  15085  fiinopn  15107  cnpfval  15298  iscnp3  15306  cnprcl2k  15309  tgcn  15311  lmbr  15316  lmbr2  15317  lmbrf  15318  lmss  15349  cnmptcom  15401  metss  15597  metcnp  15615  metcnpi  15618  metcnpi2  15619  elcncf  15676  cncfi  15681  rescncf  15684  cncfco  15694  cdivcncfap  15707  ellimc3apf  15763  limcdifap  15765  limcmpted  15766  limcimo  15768  limcresi  15769  cnplimclemr  15772  limccoap  15781  dvmptfsum  15828  plycolemc  15861  rpcxpmul2  16021  perfectlem2  16120  bcmono  16124  lgsquad2lem2  16213  eupth2fi  16732  depindlem2  16760  depindlem3  16761  bdbm1.3ii  16929  bj-2inf  16976  bj-omtrans  16994  exmidcon  17049  exmidpeirce  17050  wexmiddiffilem  17055  nninfalllem1  17063  nninfsellemdc  17065  nninfsellemqall  17070