Theorem imbi2d 611

Description: Deduction adding an antecedent to both sides of a logical equivalence.

Hypothesis

Ref	Expression
bid.1	|- (ph -> (ps <-> ch))

Assertion

Ref	Expression
imbi2d	|- (ph -> ((th -> ps) <-> (th -> ch)))

Proof of Theorem imbi2d

Step	Hyp	Ref	Expression
1		bid.1	. . 3 |- (ph -> (ps <-> ch))
2	1	a1d 12	. 2 |- (ph -> (th -> (ps <-> ch)))
3	2	pm5.74d 584	1 |- (ph -> ((th -> ps) <-> (th -> ch)))

Syntax hints:   -> wi 3   <-> wb 146

This theorem is referenced by:  imbi1d 612  orbi2d 613  bibi2d 617  imbi12d 625  pm5.42 651  dedlem0a 759  con3th 765  19.23t 1114  ax11v2 1213  sbcom 1256  sbcom2 1332  ax15 1357  ax11eq 1361  ax11el 1362  ax11indalem 1366  ax11inda2ALT 1367  ax11inda 1369  mo 1391  2mo 1445  2eu6 1452  ralcom2 1773  2gencl 1825  3gencl 1826  vtocl2gf 1845  vtocl2ga 1849  vtocl3ga 1850  mo2icl 1919  reu7 1931  sbc5g 1950  sbc6g 1951  sbcel1gv 1976  sbcel2gv 1977  uniiunlem 2128  r19.36zv 2350  dedth2h 2383  dedth3h 2384  dedth4h 2385  elint 2534  elinti 2537  elintrabg 2541  intab 2555  trel 2682  trss 2684  axrep1 2689  axrep2 2690  axrep3 2691  bm1.3ii 2701  opthgg 2784  pocl 2839  solin 2852  reuuni2f 2878  freq1 2917  dfom2 3128  elom 3129  elomg 3130  findsg 3152  finds2 3153  tfindsg 3157  tfinds2 3160  tfinds3 3161  vtoclr 3206  2optocl 3231  3optocl 3232  resieq 3368  funimaexg 3567  funopfvg 3743  fnbrfvb 3744  funbrfvbg 3748  fvelima 3755  fnressn 3828  fressnfv 3829  f1fveq 3867  tfrlem1 3902  tfr3 3917  ndmoprcl 4036  caoprcan 4047  caoprord 4048  oaordi 4170  oeordi 4204  nnacl 4219  nnmcl 4220  nnecl 4221  nnacom 4223  nnmsucr 4230  nnmcom 4231  oaabs 4242  2ecoptocl 4294  3ecoptocl 4295  th3qlem2 4305  xpdom1g 4430  supeq1 4555  supub 4560  suplub 4561  inf3lem2 4594  inf3lem5 4597  tz9.1 4626  r1pw 4666  cplem2 4701  karden 4706  aceq4 4714  aceq5lem5 4719  aceq6a 4721  aceq6b 4722  kmlem2 4746  kmlem13 4757  axrepnd 4926  axpowndlem3 4931  zfcndrep 4946  elnp 5072  prlem934a 5117  prlem934 5119  supexpr 5143  suppsr 5202  supsrlem6 5210  supre 5240  divmult 5684  divclt 5689  divcan1t 5697  divcan2t 5698  divrect 5710  divdirt 5721  divcan3t 5726  redivclt 5764  ltmul1t 5794  ltdiv1t 5813  ltmuldivt 5825  nn1suc 5895  nnaddclt 5896  nnmulclt 5897  nnleltp1t 5909  infm3 6009  infmsup 6023  xrsupsslem 6031  xrinfmsslem 6032  xrsupss 6033  xrinfmss 6034  uzind2 6162  uzindOLD 6164  uzwo4OLD 6166  zmax 6176  flval2t 6189  monoord 6239  om2uzlt 6243  seq1rn2 6266  ser1add2 6283  uzaddclt 6389  uzwo 6395  uzwoOLD 6396  nnwof 6399  indstr 6401  seqzrn2 6496  expcllem 6515  expeq0t 6525  expgt0t 6528  expgt1t 6531  mulexpt 6533  recexpt 6534  expaddt 6535  expmult 6536  expmwordit 6545  bernneq 6591  replimt 6700  cjexpt 6760  absdivt 6803  absexpt 6811  cjdivt 6835  seq1bnd 6855  cau3ir 6860  cvg2 6867  caubnd 6871  ser1absdiflem 6874  facdivt 6887  faclbnd 6890  faclbnd4lem4 6896  faclbnd6 6899  clim 6923  fsumconst 6984  bcxmas 7022  clm3 7025  clm4le 7027  clm0 7029  clmnns 7030  clm0nns 7031  clmi1 7032  clm4at 7036  clmi2at 7037  climfnn 7038  2climnn 7047  2climnn0 7048  climres 7050  iserzshft2 7052  climmulc2 7073  iserzex 7090  climubi 7097  climcau 7100  caucvglem1 7101  caucvg 7107  caucvg3t 7112  ser1cmp2 7121  cvgcmp3cetlem1 7132  cvgcmp3cetlem2 7133  expcnvlem5 7174  expcnv 7176  cvgratlem1ALT 7190  cvgratlem2ALT 7191  cvgratlem3ALT 7192  cvgratlem1 7193  cvgratlem3 7195  elcncf 7208  negfcncf 7212  rescncf 7215  ivthlem2 7225  ef0lem 7260  efaddlem27 7314  efexpt 7322  eftlext 7328  demoivre 7434  acdc3 7437  acdc5 7443  cnpfval 7707  iscnp2 7711  ishaus 7733  metcnp2 7840  metcnpi 7842  metcnpi2 7843  metcni 7846  metcnp3 7848  metcnss 7850  cncfmet 7857  lmfval 7877  caufval 7878  lmbr 7880  lmbrf 7882  lmcvg 7884  iscau 7888  iscauf 7891  iscau5 7893  lmbrnns 7894  lmcvgnns 7895  lmss 7904  causs 7906  lmclim 7914  lmcau 7946  cncms 7948  bcthlem17 7965  bcthlem18 7966  ringid 8097  isnvlem 8181  nvi 8185  va1cnlem 8292  sm1cnilem 8294  nmobndi 8383  nmounbi 8384  nmblolbi 8404  ipasslem1 8434  ipassi 8445  minveclem9 8497  minveclem24 8512  minveclem28 8516  spwmo 8598  axgroth3 8718  axgroth4 8719  h2hcau 8788  h2hlm 8789  hcau 8990  hcau2 8994  hlim 8995  hlim2 8999  hhcms 9011  hlimcaui 9045  hlimunii 9047  hhsscms 9089  occllem6 9117  projlem7 9131  projlem20 9144  projlem28 9152  projlem29 9153  pjthlem14 9170  pjtheut 9174  elspansn2t 9429  pjige0t 9576  pjcjt2 9577  pjopytht 9605  elcnopt 9723  elcnfnt 9749  cnopct 9776  cnfnct 9793  nmbdoplbt 9888  nmcoplbt 9898  lnfnmult 9915  nmbdfnlbt 9917  nmcfnlbt 9927  cnlnadjlem5 9942  pjss2co 10030  pjssmt 10031  stelt 10079  hstelt 10080  stcltr1 10139  mdbrt 10159  dmdbrt 10164  mddmd 10173  mdslmd1lem3 10191  mdslmd1lem4 10192  elat2 10204  atcvat2t 10253  cdj1 10294  ghomf1olem 10330  fveleq 10349  hmphre 10453  homcard 10462  fillsb 10471  filint2 10482  dtt2 10498  isded 10549  dedi 10550  iscat 10567  cati 10568  isfunb 10629

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7

This theorem depends on definitions:  df-bi 147  df-an 225

Copyright terms: Public domain