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  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  9287  nnaddcl  9324  nnmulcl  9325  zaddcllempos  9681  zaddcllemneg  9683  prime  9745  peano5uzti  9754  uzind2  9758  zindd  9764  uzaddcl  9986  exfzdc  10659  infssuzex  10666  nninfdcex  10672  frec2uzltd  10840  frec2uzrdg  10846  frecuzrdgtcl  10849  frecuzrdgg  10853  frecuzrdgfunlem  10856  seq3val  10897  seqvalcd  10898  seq3clss  10908  seq3fveq2  10912  seqfveq2g  10914  seq3shft2  10918  seqshft2g  10919  monoord  10922  seq3split  10925  seqsplitg  10926  seq3caopr3  10928  seqcaopr3g  10929  seq3f1olemp  10952  seqf1oglem2a  10955  seqf1og  10958  seq3id3  10961  seq3id2  10963  seq3homo  10964  seq3z  10965  seqhomog  10967  seqfeq4g  10968  ser3ge0  10973  exp3vallem  10977  expcllem  10987  expap0  11006  mulexp  11015  expadd  11018  expmul  11021  leexp2r  11030  leexp1a  11031  bernneq  11098  modqexp  11104  nn0ltexp2  11147  apexp1  11156  facdiv  11176  faclbnd  11179  faclbnd6  11182  omgadd  11242  hashmap  11268  hashf1  11287  seq3coll  11294  wrdind  11494  wrd2ind  11495  pfxccatin12lem3  11504  shftvalg  11601  shftval4g  11602  cjexp  11658  resqrexlemover  11776  resqrexlemdecn  11778  resqrexlemlo  11779  resqrexlemcalc3  11782  absexp  11845  climshft  12070  climub  12110  climserle  12111  fsum2d  12202  fsumabs  12232  fsumiun  12244  binom  12251  bcxmas  12256  cvgratnnlemnexp  12291  cvgratnnlemmn  12292  clim2prod  12306  prodfap0  12312  prodfrecap  12313  fprodabs  12383  fprod2d  12390  demoivreALT  12541  dvdsfac  12627  bitsinv1  12729  bezoutlemstep  12774  bezoutlemmain  12775  bezoutlemex  12778  dfgcd2  12791  gcdmultiple  12797  rplpwr  12804  nn0seqcvgd  12819  alginv  12825  algcvga  12829  algfx  12830  isprm4  12897  prmind2  12898  prmdvdsexp  12926  prmfac1  12930  eulerthlemrprm  13007  eulerthlema  13008  reumodprminv  13032  pcmpt  13122  pcfac  13129  prmpwdvds  13134  ennnfoneleminc  13302  ennnfonelemkh  13303  ennnfonelemhf1o  13304  ennnfonelemhom  13306  nninfdclemlt  13342  mulgnnass  13960  mhmmulg  13966  gzsumconst  14143  srgmulgass  14293  srgpcomp  14294  lmodvsmmulgdi  14660  cnfldexp  14914  assamulgscm  15043  mplelbascoe  15083  fiinopn  15105  cnpfval  15296  iscnp3  15304  cnprcl2k  15307  tgcn  15309  lmbr  15314  lmbr2  15315  lmbrf  15316  lmss  15347  cnmptcom  15399  metss  15595  metcnp  15613  metcnpi  15616  metcnpi2  15617  elcncf  15674  cncfi  15679  rescncf  15682  cncfco  15692  cdivcncfap  15705  ellimc3apf  15761  limcdifap  15763  limcmpted  15764  limcimo  15766  limcresi  15767  cnplimclemr  15770  limccoap  15779  dvmptfsum  15826  plycolemc  15859  rpcxpmul2  16015  perfectlem2  16114  lgsquad2lem2  16201  eupth2fi  16720  depindlem2  16748  depindlem3  16749  bdbm1.3ii  16917  bj-2inf  16964  bj-omtrans  16982  exmidcon  17037  exmidpeirce  17038  wexmiddiffilem  17043  nninfalllem1  17051  nninfsellemdc  17053  nninfsellemqall  17058