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  9289  nnaddcl  9326  nnmulcl  9327  zaddcllempos  9685  zaddcllemneg  9687  prime  9749  peano5uzti  9758  uzind2  9762  zindd  9768  uzaddcl  9995  exfzdc  10669  infssuzex  10676  nninfdcex  10682  frec2uzltd  10853  frec2uzrdg  10859  frecuzrdgtcl  10862  frecuzrdgg  10866  frecuzrdgfunlem  10869  seq3val  10910  seqvalcd  10911  seq3clss  10921  seq3fveq2  10925  seqfveq2g  10927  seq3shft2  10931  seqshft2g  10932  monoord  10935  seq3split  10938  seqsplitg  10939  seq3caopr3  10941  seqcaopr3g  10942  seq3f1olemp  10965  seqf1oglem2a  10968  seqf1og  10971  seq3id3  10974  seq3id2  10976  seq3homo  10977  seq3z  10978  seqhomog  10980  seqfeq4g  10981  ser3ge0  10986  exp3vallem  10990  expcllem  11000  expap0  11019  mulexp  11028  expadd  11031  expmul  11034  leexp2r  11043  leexp1a  11044  bernneq  11111  modqexp  11117  nn0ltexp2  11161  apexp1  11170  facdiv  11190  faclbnd  11193  faclbnd6  11196  omgadd  11256  hashmap  11282  hashf1  11301  seq3coll  11308  wrdind  11508  wrd2ind  11509  pfxccatin12lem3  11518  shftvalg  11615  shftval4g  11616  cjexp  11672  resqrexlemover  11790  resqrexlemdecn  11792  resqrexlemlo  11793  resqrexlemcalc3  11796  absexp  11860  climshft  12086  climub  12126  climserle  12127  fsum2d  12218  fsumabs  12248  fsumiun  12260  binom  12267  bcxmas  12272  cvgratnnlemnexp  12307  cvgratnnlemmn  12308  clim2prod  12322  prodfap0  12328  prodfrecap  12329  fprodabs  12399  fprod2d  12406  demoivreALT  12557  dvdsfac  12643  bitsinv1  12745  bezoutlemstep  12790  bezoutlemmain  12791  bezoutlemex  12794  dfgcd2  12807  gcdmultiple  12813  rplpwr  12820  nn0seqcvgd  12835  alginv  12841  algcvga  12845  algfx  12846  isprm4  12913  prmind2  12914  prmdvdsexp  12943  prmfac1  12947  eulerthlemrprm  13027  eulerthlema  13028  reumodprminv  13052  pcmpt  13142  pcfac  13149  prmpwdvds  13154  prmlem1a  13241  ennnfoneleminc  13351  ennnfonelemkh  13352  ennnfonelemhf1o  13353  ennnfonelemhom  13355  nninfdclemlt  13391  mulgnnass  14009  mhmmulg  14015  gzsumconst  14192  srgmulgass  14342  srgpcomp  14343  lmodvsmmulgdi  14709  cnfldexp  14963  assamulgscm  15092  mplelbascoe  15132  fiinopn  15154  cnpfval  15345  iscnp3  15353  cnprcl2k  15356  tgcn  15358  lmbr  15363  lmbr2  15364  lmbrf  15365  lmss  15396  cnmptcom  15448  metss  15644  metcnp  15662  metcnpi  15665  metcnpi2  15666  elcncf  15723  cncfi  15728  rescncf  15731  cncfco  15741  cdivcncfap  15754  ellimc3apf  15810  limcdifap  15812  limcmpted  15813  limcimo  15815  limcresi  15816  cnplimclemr  15819  limccoap  15828  dvmptfsum  15875  plycolemc  15908  rpcxpmul2  16068  perfectlem2  16198  bcmono  16202  bposlem5  16213  lgsquad2lem2  16299  eupth2fi  16818  depindlem2  16846  depindlem3  16847  bdbm1.3ii  17015  bj-2inf  17062  bj-omtrans  17080  exmidcon  17135  exmidpeirce  17136  wexmiddiffilem  17141  nninfalllem1  17149  nninfsellemdc  17151  nninfsellemqall  17156