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  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  3893  elint  3971  elintrabg  3978  intab  3994  trss  4233  bm1.3ii  4249  pocl  4443  swopolem  4445  sowlin  4460  frforeq3  4487  frirrg  4490  frind  4492  reusv3  4601  regexmid  4677  ordsoexmid  4704  tfisi  4729  finds2  4743  nnregexmid  4763  vtoclr  4818  2optocl  4847  3optocl  4848  raliunxp  4916  resieq  5068  iss  5104  cnveqb  5238  iotaexab  5351  funmo  5387  fnbrfvb  5735  fvelimab  5753  fvmptssdm  5784  fmptco  5865  fnressn  5892  fressnfv  5893  isoselem  6016  isosolem  6020  ovg  6218  caovcan  6244  caovordig  6245  caovord  6251  f1o2ndf1  6454  poxp  6458  smoeq  6551  smores  6553  tfrlem1  6569  tfrlemi1  6593  tfrexlem  6595  tfri3  6628  oawordriexmid  6733  nnacl  6743  nnmcl  6744  nnacom  6747  nnaass  6748  nndi  6749  nnmass  6750  nnmsucr  6751  nnmcom  6752  nnsucsssuc  6755  nntri3or  6756  nnaordi  6771  nnaword  6774  nnmordi  6779  nnaordex  6791  2ecoptocl  6887  3ecoptocl  6888  th3qlem2  6902  xpdom2g  7120  findcard2  7183  findcard2s  7184  xpfi  7229  supeq1  7316  ordiso2  7365  updjud  7412  nnnninfeq  7458  exmidontriimlem4  7570  exmidontriim  7571  papcotr  7603  distrnq0  7816  addassnq0  7819  elinp  7831  prcdnql  7841  prcunqu  7842  prarloclem3  7854  caucvgpr  8039  caucvgprpr  8069  ltsosr  8121  caucvgsrlemcau  8150  caucvgsrlemgt1  8152  caucvgsrlemoffres  8157  pitonn  8205  axpre-ltwlin  8240  axcaucvglemres  8256  sup3exmid  9277  nnaddcl  9303  nnmulcl  9304  zaddcllempos  9660  zaddcllemneg  9662  prime  9724  peano5uzti  9733  uzind2  9737  zindd  9743  uzaddcl  9965  exfzdc  10637  infssuzex  10644  nninfdcex  10650  frec2uzltd  10818  frec2uzrdg  10824  frecuzrdgtcl  10827  frecuzrdgg  10831  frecuzrdgfunlem  10834  seq3val  10875  seqvalcd  10876  seq3clss  10886  seq3fveq2  10890  seqfveq2g  10892  seq3shft2  10896  seqshft2g  10897  monoord  10900  seq3split  10903  seqsplitg  10904  seq3caopr3  10906  seqcaopr3g  10907  seq3f1olemp  10930  seqf1oglem2a  10933  seqf1og  10936  seq3id3  10939  seq3id2  10941  seq3homo  10942  seq3z  10943  seqhomog  10945  seqfeq4g  10946  ser3ge0  10951  exp3vallem  10955  expcllem  10965  expap0  10984  mulexp  10993  expadd  10996  expmul  10999  leexp2r  11008  leexp1a  11009  bernneq  11076  modqexp  11082  nn0ltexp2  11125  apexp1  11134  facdiv  11154  faclbnd  11157  faclbnd6  11160  omgadd  11220  hashmap  11246  hashf1  11265  seq3coll  11272  wrdind  11472  wrd2ind  11473  pfxccatin12lem3  11482  shftvalg  11579  shftval4g  11580  cjexp  11636  resqrexlemover  11754  resqrexlemdecn  11756  resqrexlemlo  11757  resqrexlemcalc3  11760  absexp  11823  climshft  12048  climub  12088  climserle  12089  fsum2d  12180  fsumabs  12210  fsumiun  12222  binom  12229  bcxmas  12234  cvgratnnlemnexp  12269  cvgratnnlemmn  12270  clim2prod  12284  prodfap0  12290  prodfrecap  12291  fprodabs  12361  fprod2d  12368  demoivreALT  12519  dvdsfac  12605  bitsinv1  12707  bezoutlemstep  12752  bezoutlemmain  12753  bezoutlemex  12756  dfgcd2  12769  gcdmultiple  12775  rplpwr  12782  nn0seqcvgd  12797  alginv  12803  algcvga  12807  algfx  12808  isprm4  12875  prmind2  12876  prmdvdsexp  12904  prmfac1  12908  eulerthlemrprm  12985  eulerthlema  12986  reumodprminv  13010  pcmpt  13100  pcfac  13107  prmpwdvds  13112  ennnfoneleminc  13280  ennnfonelemkh  13281  ennnfonelemhf1o  13282  ennnfonelemhom  13284  nninfdclemlt  13320  mulgnnass  13937  mhmmulg  13943  gzsumconst  14120  srgmulgass  14267  srgpcomp  14268  lmodvsmmulgdi  14632  cnfldexp  14886  mplelbascoe  15006  fiinopn  15028  cnpfval  15219  iscnp3  15227  cnprcl2k  15230  tgcn  15232  lmbr  15237  lmbr2  15238  lmbrf  15239  lmss  15270  cnmptcom  15322  metss  15518  metcnp  15536  metcnpi  15539  metcnpi2  15540  elcncf  15597  cncfi  15602  rescncf  15605  cncfco  15615  cdivcncfap  15628  ellimc3apf  15684  limcdifap  15686  limcmpted  15687  limcimo  15689  limcresi  15690  cnplimclemr  15693  limccoap  15702  dvmptfsum  15749  plycolemc  15782  rpcxpmul2  15938  perfectlem2  16028  lgsquad2lem2  16115  eupth2fi  16634  depindlem2  16662  depindlem3  16663  bdbm1.3ii  16831  bj-2inf  16878  bj-omtrans  16896  exmidcon  16950  exmidpeirce  16951  nninfalllem1  16956  nninfsellemdc  16958  nninfsellemqall  16963