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  6566  smores  6568  tfrlem1  6584  tfrlemi1  6608  tfrexlem  6610  tfri3  6643  oawordriexmid  6748  nnacl  6758  nnmcl  6759  nnacom  6762  nnaass  6763  nndi  6764  nnmass  6765  nnmsucr  6766  nnmcom  6767  nnsucsssuc  6770  nntri3or  6771  nnaordi  6786  nnaword  6789  nnmordi  6794  nnaordex  6806  2ecoptocl  6902  3ecoptocl  6903  th3qlem2  6917  xpdom2g  7136  findcard2  7199  findcard2s  7200  xpfi  7245  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  9690  zaddcllemneg  9692  prime  9755  peano5uzti  9764  uzind2  9768  zindd  9774  uzaddcl  10001  exfzdc  10675  infssuzex  10682  nninfdcex  10688  frec2uzltd  10860  frec2uzrdg  10866  frecuzrdgtcl  10869  frecuzrdgg  10873  frecuzrdgfunlem  10876  seq3val  10917  seqvalcd  10918  seq3clss  10928  seq3fveq2  10932  seqfveq2g  10934  seq3shft2  10938  seqshft2g  10939  monoord  10942  seq3split  10945  seqsplitg  10946  seq3caopr3  10948  seqcaopr3g  10949  seq3f1olemp  10972  seqf1oglem2a  10975  seqf1og  10978  seq3id3  10981  seq3id2  10983  seq3homo  10984  seq3z  10985  seqhomog  10987  seqfeq4g  10988  ser3ge0  10993  exp3vallem  10997  expcllem  11007  expap0  11026  mulexp  11035  expadd  11038  expmul  11041  leexp2r  11050  leexp1a  11051  bernneq  11118  modqexp  11124  nn0ltexp2  11168  apexp1  11177  facdiv  11197  faclbnd  11200  faclbnd6  11203  omgadd  11263  hashmap  11289  hashf1  11308  seq3coll  11315  wrdind  11515  wrd2ind  11516  pfxccatin12lem3  11525  shftvalg  11622  shftval4g  11623  cjexp  11679  resqrexlemover  11797  resqrexlemdecn  11799  resqrexlemlo  11800  resqrexlemcalc3  11803  absexp  11867  climshft  12094  climub  12134  climserle  12135  fsum2d  12226  fsumabs  12256  fsumiun  12268  binom  12275  bcxmas  12280  cvgratnnlemnexp  12315  cvgratnnlemmn  12316  clim2prod  12330  prodfap0  12336  prodfrecap  12337  fprodabs  12407  fprod2d  12414  demoivreALT  12565  dvdsfac  12651  bitsinv1  12753  bezoutlemstep  12798  bezoutlemmain  12799  bezoutlemex  12802  dfgcd2  12815  gcdmultiple  12821  rplpwr  12828  nn0seqcvgd  12843  alginv  12849  algcvga  12853  algfx  12854  isprm4  12921  prmind2  12922  prmdvdsexp  12951  prmfac1  12955  eulerthlemrprm  13035  eulerthlema  13036  reumodprminv  13060  pcmpt  13150  pcfac  13157  prmpwdvds  13162  prmlem1a  13249  ennnfoneleminc  13359  ennnfonelemkh  13360  ennnfonelemhf1o  13361  ennnfonelemhom  13363  nninfdclemlt  13399  mulgnnass  14018  mhmmulg  14024  gzsumconst  14232  gsumcom2fi  14274  srgmulgass  14399  srgpcomp  14400  lmodvsmmulgdi  14768  cnfldexp  15022  assamulgscm  15151  fiinopn  15247  cnpfval  15438  iscnp3  15446  cnprcl2k  15449  tgcn  15451  lmbr  15456  lmbr2  15457  lmbrf  15458  lmss  15489  cnmptcom  15541  metss  15737  metcnp  15755  metcnpi  15758  metcnpi2  15759  elcncf  15816  cncfi  15821  rescncf  15824  cncfco  15834  cdivcncfap  15847  ellimc3apf  15903  limcdifap  15905  limcmpted  15906  limcimo  15908  limcresi  15909  cnplimclemr  15912  limccoap  15921  dvmptfsum  15968  plycolemc  16001  rpcxpmul2  16163  perfectlem2  16317  bcmono  16321  bposlem5  16332  lgsquad2lem2  16423  eupth2fi  16942  depindlem2  16970  depindlem3  16971  bdbm1.3ii  17139  bj-2inf  17186  bj-omtrans  17204  exmidcon  17259  exmidpeirce  17260  wexmiddiffilem  17265  nninfalllem1  17274  nninfsellemdc  17276  nninfsellemqall  17281