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  4240  bm1.3ii  4256  pocl  4450  swopolem  4452  sowlin  4467  frforeq3  4494  frirrg  4497  frind  4499  reusv3  4608  regexmid  4684  ordsoexmid  4711  tfisi  4736  finds2  4750  nnregexmid  4770  vtoclr  4825  2optocl  4854  3optocl  4855  raliunxp  4923  resieq  5075  iss  5112  cnveqb  5246  iotaexab  5359  funmo  5395  fnbrfvb  5744  fvelimab  5762  fvmptssdm  5793  fmptco  5877  fnressn  5904  fressnfv  5905  isoselem  6029  isosolem  6033  ovg  6231  caovcan  6257  caovordig  6258  caovord  6264  f1o2ndf1  6468  poxp  6472  smoeq  6565  smores  6567  tfrlem1  6583  tfrlemi1  6607  tfrexlem  6609  tfri3  6642  oawordriexmid  6747  nnacl  6757  nnmcl  6758  nnacom  6761  nnaass  6762  nndi  6763  nnmass  6764  nnmsucr  6765  nnmcom  6766  nnsucsssuc  6769  nntri3or  6770  nnaordi  6785  nnaword  6788  nnmordi  6793  nnaordex  6805  2ecoptocl  6901  3ecoptocl  6902  th3qlem2  6916  xpdom2g  7134  findcard2  7197  findcard2s  7198  xpfi  7243  supeq1  7332  ordiso2  7381  updjud  7428  nnnninfeq  7474  exmidontriimlem4  7586  exmidontriim  7587  papcotr  7619  distrnq0  7832  addassnq0  7835  elinp  7847  prcdnql  7857  prcunqu  7858  prarloclem3  7870  caucvgpr  8055  caucvgprpr  8085  ltsosr  8137  caucvgsrlemcau  8166  caucvgsrlemgt1  8168  caucvgsrlemoffres  8173  pitonn  8221  axpre-ltwlin  8256  axcaucvglemres  8272  sup3exmid  9295  nnaddcl  9333  nnmulcl  9334  zaddcllempos  9692  zaddcllemneg  9694  prime  9756  peano5uzti  9765  uzind2  9769  zindd  9775  uzaddcl  10002  exfzdc  10676  infssuzex  10683  nninfdcex  10689  frec2uzltd  10861  frec2uzrdg  10867  frecuzrdgtcl  10870  frecuzrdgg  10874  frecuzrdgfunlem  10877  seq3val  10918  seqvalcd  10919  seq3clss  10929  seq3fveq2  10933  seqfveq2g  10935  seq3shft2  10939  seqshft2g  10940  monoord  10943  seq3split  10946  seqsplitg  10947  seq3caopr3  10949  seqcaopr3g  10950  seq3f1olemp  10973  seqf1oglem2a  10976  seqf1og  10979  seq3id3  10982  seq3id2  10984  seq3homo  10985  seq3z  10986  seqhomog  10988  seqfeq4g  10989  ser3ge0  10994  exp3vallem  10998  expcllem  11008  expap0  11027  mulexp  11036  expadd  11039  expmul  11042  leexp2r  11051  leexp1a  11052  bernneq  11119  modqexp  11125  nn0ltexp2  11169  apexp1  11178  facdiv  11198  faclbnd  11201  faclbnd6  11204  omgadd  11264  hashmap  11290  hashf1  11309  seq3coll  11316  wrdind  11516  wrd2ind  11517  pfxccatin12lem3  11526  shftvalg  11623  shftval4g  11624  cjexp  11680  resqrexlemover  11798  resqrexlemdecn  11800  resqrexlemlo  11801  resqrexlemcalc3  11804  absexp  11868  climshft  12095  climub  12135  climserle  12136  fsum2d  12227  fsumabs  12257  fsumiun  12269  binom  12276  bcxmas  12281  cvgratnnlemnexp  12316  cvgratnnlemmn  12317  clim2prod  12331  prodfap0  12337  prodfrecap  12338  fprodabs  12408  fprod2d  12415  demoivreALT  12566  dvdsfac  12652  bitsinv1  12754  bezoutlemstep  12799  bezoutlemmain  12800  bezoutlemex  12803  dfgcd2  12816  gcdmultiple  12822  rplpwr  12829  nn0seqcvgd  12844  alginv  12850  algcvga  12854  algfx  12855  isprm4  12922  prmind2  12923  prmdvdsexp  12952  prmfac1  12956  eulerthlemrprm  13036  eulerthlema  13037  reumodprminv  13061  pcmpt  13151  pcfac  13158  prmpwdvds  13163  prmlem1a  13250  ennnfoneleminc  13360  ennnfonelemkh  13361  ennnfonelemhf1o  13362  ennnfonelemhom  13364  nninfdclemlt  13400  mulgnnass  14019  mhmmulg  14025  gzsumconst  14233  gsumcom2fi  14275  srgmulgass  14400  srgpcomp  14401  lmodvsmmulgdi  14769  cnfldexp  15023  assamulgscm  15152  mplelbascoe  15205  fiinopn  15227  cnpfval  15418  iscnp3  15426  cnprcl2k  15429  tgcn  15431  lmbr  15436  lmbr2  15437  lmbrf  15438  lmss  15469  cnmptcom  15521  metss  15717  metcnp  15735  metcnpi  15738  metcnpi2  15739  elcncf  15796  cncfi  15801  rescncf  15804  cncfco  15814  cdivcncfap  15827  ellimc3apf  15883  limcdifap  15885  limcmpted  15886  limcimo  15888  limcresi  15889  cnplimclemr  15892  limccoap  15901  dvmptfsum  15948  plycolemc  15981  rpcxpmul2  16143  perfectlem2  16297  bcmono  16301  bposlem5  16312  lgsquad2lem2  16403  eupth2fi  16922  depindlem2  16950  depindlem3  16951  bdbm1.3ii  17119  bj-2inf  17166  bj-omtrans  17184  exmidcon  17239  exmidpeirce  17240  wexmiddiffilem  17245  nninfalllem1  17254  nninfsellemdc  17256  nninfsellemqall  17261