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	|- ( ph -> ( ps <-> ch ) )

Assertion

Ref	Expression
imbi2d	|- ( ph -> ( ( th -> ps ) <-> ( th -> ch ) ) )

Proof of Theorem imbi2d

Step	Hyp	Ref	Expression
1		imbid.1	. . 3 |- ( ph -> ( ps <-> ch ) )
2	1	a1d 22	. 2 |- ( ph -> ( th -> ( ps <-> ch ) ) )
3	2	pm5.74d 182	1 |- ( ph -> ( ( th -> ps ) <-> ( th -> ch ) ) )

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  1868  ax11v  1875  equs5or  1878  mo23  2121  nfabdw  2394  2gencl  2837  3gencl  2838  vtocl2gf  2867  vtocl3gf  2868  vtocl4g  2876  vtocl4ga  2877  eqeu  2977  mo2icl  2986  euind  2994  reu7  3002  reuind  3012  sbctt  3099  reu8nf  3114  sbcnestgf  3180  preq12bg  3861  elint  3939  elintrabg  3946  intab  3962  trss  4201  bm1.3ii  4215  pocl  4406  swopolem  4408  sowlin  4423  frforeq3  4450  frirrg  4453  frind  4455  reusv3  4563  regexmid  4639  ordsoexmid  4666  tfisi  4691  finds2  4705  nnregexmid  4725  vtoclr  4780  2optocl  4809  3optocl  4810  raliunxp  4877  resieq  5029  iss  5065  cnveqb  5199  iotaexab  5312  funmo  5348  fnbrfvb  5693  fvelimab  5711  fvmptssdm  5740  fmptco  5821  fnressn  5848  fressnfv  5849  isoselem  5971  isosolem  5975  ovg  6171  caovcan  6197  caovordig  6198  caovord  6204  f1o2ndf1  6402  poxp  6406  smoeq  6499  smores  6501  tfrlem1  6517  tfrlemi1  6541  tfrexlem  6543  tfri3  6576  oawordriexmid  6681  nnacl  6691  nnmcl  6692  nnacom  6695  nnaass  6696  nndi  6697  nnmass  6698  nnmsucr  6699  nnmcom  6700  nnsucsssuc  6703  nntri3or  6704  nnaordi  6719  nnaword  6722  nnmordi  6727  nnaordex  6739  2ecoptocl  6835  3ecoptocl  6836  th3qlem2  6850  xpdom2g  7059  findcard2  7121  findcard2s  7122  xpfi  7167  supeq1  7245  ordiso2  7294  updjud  7341  nnnninfeq  7387  exmidontriimlem4  7499  exmidontriim  7500  distrnq0  7739  addassnq0  7742  elinp  7754  prcdnql  7764  prcunqu  7765  prarloclem3  7777  caucvgpr  7962  caucvgprpr  7992  ltsosr  8044  caucvgsrlemcau  8073  caucvgsrlemgt1  8075  caucvgsrlemoffres  8080  pitonn  8128  axpre-ltwlin  8163  axcaucvglemres  8179  sup3exmid  9196  nnaddcl  9222  nnmulcl  9223  zaddcllempos  9577  zaddcllemneg  9579  prime  9640  peano5uzti  9649  uzind2  9653  zindd  9659  uzaddcl  9881  exfzdc  10549  infssuzex  10556  nninfdcex  10560  frec2uzltd  10728  frec2uzrdg  10734  frecuzrdgtcl  10737  frecuzrdgg  10741  frecuzrdgfunlem  10744  seq3val  10785  seqvalcd  10786  seq3clss  10796  seq3fveq2  10800  seqfveq2g  10802  seq3shft2  10806  seqshft2g  10807  monoord  10810  seq3split  10813  seqsplitg  10814  seq3caopr3  10816  seqcaopr3g  10817  seq3f1olemp  10840  seqf1oglem2a  10843  seqf1og  10846  seq3id3  10849  seq3id2  10851  seq3homo  10852  seq3z  10853  seqhomog  10855  seqfeq4g  10856  ser3ge0  10861  exp3vallem  10865  expcllem  10875  expap0  10894  mulexp  10903  expadd  10906  expmul  10909  leexp2r  10918  leexp1a  10919  bernneq  10985  modqexp  10991  nn0ltexp2  11034  apexp1  11043  facdiv  11063  faclbnd  11066  faclbnd6  11069  omgadd  11128  seq3coll  11169  wrdind  11369  wrd2ind  11370  pfxccatin12lem3  11379  shftvalg  11476  shftval4g  11477  cjexp  11533  resqrexlemover  11650  resqrexlemdecn  11652  resqrexlemlo  11653  resqrexlemcalc3  11656  absexp  11719  climshft  11944  climub  11984  climserle  11985  fsum2d  12076  fsumabs  12106  fsumiun  12118  binom  12125  bcxmas  12130  cvgratnnlemnexp  12165  cvgratnnlemmn  12166  clim2prod  12180  prodfap0  12186  prodfrecap  12187  fprodabs  12257  fprod2d  12264  demoivreALT  12415  dvdsfac  12501  bitsinv1  12603  bezoutlemstep  12648  bezoutlemmain  12649  bezoutlemex  12652  dfgcd2  12665  gcdmultiple  12671  rplpwr  12678  nn0seqcvgd  12693  alginv  12699  algcvga  12703  algfx  12704  isprm4  12771  prmind2  12772  prmdvdsexp  12800  prmfac1  12804  eulerthlemrprm  12881  eulerthlema  12882  reumodprminv  12906  pcmpt  12996  pcfac  13003  prmpwdvds  13008  ennnfoneleminc  13112  ennnfonelemkh  13113  ennnfonelemhf1o  13114  ennnfonelemhom  13116  nninfdclemlt  13152  gsumfzz  13658  mulgnnass  13824  mhmmulg  13830  gsumfzconst  14008  srgmulgass  14083  srgpcomp  14084  lmodvsmmulgdi  14419  cnfldexp  14673  gsumfzfsumlemm  14683  mplelbascoe  14793  fiinopn  14815  cnpfval  15006  iscnp3  15014  cnprcl2k  15017  tgcn  15019  lmbr  15024  lmbr2  15025  lmbrf  15026  lmss  15057  cnmptcom  15109  metss  15305  metcnp  15323  metcnpi  15326  metcnpi2  15327  elcncf  15384  cncfi  15389  rescncf  15392  cncfco  15402  cdivcncfap  15415  ellimc3apf  15471  limcdifap  15473  limcmpted  15474  limcimo  15476  limcresi  15477  cnplimclemr  15480  limccoap  15489  dvmptfsum  15536  plycolemc  15569  rpcxpmul2  15724  perfectlem2  15814  lgsquad2lem2  15901  eupth2fi  16420  depindlem2  16448  depindlem3  16449  bdbm1.3ii  16607  bj-2inf  16654  bj-omtrans  16672  exmidcon  16728  exmidpeirce  16729  nninfalllem1  16734  nninfsellemdc  16736  nninfsellemqall  16741