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  15208  fiinopn  15230  cnpfval  15421  iscnp3  15429  cnprcl2k  15432  tgcn  15434  lmbr  15439  lmbr2  15440  lmbrf  15441  lmss  15472  cnmptcom  15524  metss  15720  metcnp  15738  metcnpi  15741  metcnpi2  15742  elcncf  15799  cncfi  15804  rescncf  15807  cncfco  15817  cdivcncfap  15830  ellimc3apf  15886  limcdifap  15888  limcmpted  15889  limcimo  15891  limcresi  15892  cnplimclemr  15895  limccoap  15904  dvmptfsum  15951  plycolemc  15984  rpcxpmul2  16146  perfectlem2  16300  bcmono  16304  bposlem5  16315  lgsquad2lem2  16406  eupth2fi  16925  depindlem2  16953  depindlem3  16954  bdbm1.3ii  17122  bj-2inf  17169  bj-omtrans  17187  exmidcon  17242  exmidpeirce  17243  wexmiddiffilem  17248  nninfalllem1  17257  nninfsellemdc  17259  nninfsellemqall  17264