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 ) ) )

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  7327  ordiso2  7376  updjud  7423  nnnninfeq  7469  exmidontriimlem4  7581  exmidontriim  7582  papcotr  7614  distrnq0  7827  addassnq0  7830  elinp  7842  prcdnql  7852  prcunqu  7853  prarloclem3  7865  caucvgpr  8050  caucvgprpr  8080  ltsosr  8132  caucvgsrlemcau  8161  caucvgsrlemgt1  8163  caucvgsrlemoffres  8168  pitonn  8216  axpre-ltwlin  8251  axcaucvglemres  8267  sup3exmid  9290  nnaddcl  9327  nnmulcl  9328  zaddcllempos  9686  zaddcllemneg  9688  prime  9750  peano5uzti  9759  uzind2  9763  zindd  9769  uzaddcl  9996  exfzdc  10670  infssuzex  10677  nninfdcex  10683  frec2uzltd  10855  frec2uzrdg  10861  frecuzrdgtcl  10864  frecuzrdgg  10868  frecuzrdgfunlem  10871  seq3val  10912  seqvalcd  10913  seq3clss  10923  seq3fveq2  10927  seqfveq2g  10929  seq3shft2  10933  seqshft2g  10934  monoord  10937  seq3split  10940  seqsplitg  10941  seq3caopr3  10943  seqcaopr3g  10944  seq3f1olemp  10967  seqf1oglem2a  10970  seqf1og  10973  seq3id3  10976  seq3id2  10978  seq3homo  10979  seq3z  10980  seqhomog  10982  seqfeq4g  10983  ser3ge0  10988  exp3vallem  10992  expcllem  11002  expap0  11021  mulexp  11030  expadd  11033  expmul  11036  leexp2r  11045  leexp1a  11046  bernneq  11113  modqexp  11119  nn0ltexp2  11163  apexp1  11172  facdiv  11192  faclbnd  11195  faclbnd6  11198  omgadd  11258  hashmap  11284  hashf1  11303  seq3coll  11310  wrdind  11510  wrd2ind  11511  pfxccatin12lem3  11520  shftvalg  11617  shftval4g  11618  cjexp  11674  resqrexlemover  11792  resqrexlemdecn  11794  resqrexlemlo  11795  resqrexlemcalc3  11798  absexp  11862  climshft  12089  climub  12129  climserle  12130  fsum2d  12221  fsumabs  12251  fsumiun  12263  binom  12270  bcxmas  12275  cvgratnnlemnexp  12310  cvgratnnlemmn  12311  clim2prod  12325  prodfap0  12331  prodfrecap  12332  fprodabs  12402  fprod2d  12409  demoivreALT  12560  dvdsfac  12646  bitsinv1  12748  bezoutlemstep  12793  bezoutlemmain  12794  bezoutlemex  12797  dfgcd2  12810  gcdmultiple  12816  rplpwr  12823  nn0seqcvgd  12838  alginv  12844  algcvga  12848  algfx  12849  isprm4  12916  prmind2  12917  prmdvdsexp  12946  prmfac1  12950  eulerthlemrprm  13030  eulerthlema  13031  reumodprminv  13055  pcmpt  13145  pcfac  13152  prmpwdvds  13157  prmlem1a  13244  ennnfoneleminc  13354  ennnfonelemkh  13355  ennnfonelemhf1o  13356  ennnfonelemhom  13358  nninfdclemlt  13394  mulgnnass  14013  mhmmulg  14019  gzsumconst  14227  srgmulgass  14377  srgpcomp  14378  lmodvsmmulgdi  14744  cnfldexp  14998  assamulgscm  15127  mplelbascoe  15174  fiinopn  15196  cnpfval  15387  iscnp3  15395  cnprcl2k  15398  tgcn  15400  lmbr  15405  lmbr2  15406  lmbrf  15407  lmss  15438  cnmptcom  15490  metss  15686  metcnp  15704  metcnpi  15707  metcnpi2  15708  elcncf  15765  cncfi  15770  rescncf  15773  cncfco  15783  cdivcncfap  15796  ellimc3apf  15852  limcdifap  15854  limcmpted  15855  limcimo  15857  limcresi  15858  cnplimclemr  15861  limccoap  15870  dvmptfsum  15917  plycolemc  15950  rpcxpmul2  16110  perfectlem2  16261  bcmono  16265  bposlem5  16276  lgsquad2lem2  16367  eupth2fi  16886  depindlem2  16914  depindlem3  16915  bdbm1.3ii  17083  bj-2inf  17130  bj-omtrans  17148  exmidcon  17203  exmidpeirce  17204  wexmiddiffilem  17209  nninfalllem1  17217  nninfsellemdc  17219  nninfsellemqall  17224