Theorem imbi2d 610

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 583	1 |- (ph -> ((th -> ps) <-> (th -> ch)))

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

This theorem is referenced by:  imbi1d 611  orbi2d 612  bibi2d 616  imbi12d 624  pm5.42 650  dedlem0a 758  con3th 764  19.23t 1112  ax11v2 1210  sbcom 1253  sbcom2 1329  ax15 1352  ax11eq 1356  ax11el 1357  ax11indalem 1361  ax11inda2ALT 1362  ax11inda 1364  mo 1386  2mo 1440  2eu6 1447  ralcom2 1768  2gencl 1820  3gencl 1821  vtocl2gf 1840  vtocl2ga 1844  vtocl3ga 1845  mo2icl 1914  reu7 1925  sbc5g 1944  sbc6g 1945  sbcel1gv 1970  sbcel2gv 1971  uniiunlem 2122  r19.36zv 2344  dedth2h 2377  dedth3h 2378  dedth4h 2379  elint 2529  elinti 2532  elintrabg 2536  intab 2550  trel 2677  trss 2679  axrep1 2684  axrep2 2685  axrep3 2686  bm1.3ii 2696  opthgg 2779  pocl 2835  solin 2848  reuuni2f 2873  freq1 2912  dfom2 3123  elom 3124  elomg 3125  findsg 3147  finds2 3148  tfindsg 3152  tfinds2 3155  tfinds3 3156  vtoclr 3201  2optocl 3226  3optocl 3227  resieq 3360  funimaexg 3561  funopfvg 3737  fnbrfvb 3738  funbrfvbg 3742  fvelima 3749  fnressn 3822  fressnfv 3823  f1fveq 3861  tfrlem1 3896  tfr3 3911  ndmoprcl 4030  caoprcan 4041  caoprord 4042  oaordi 4164  oeordi 4198  nnacl 4213  nnmcl 4214  nnecl 4215  nnacom 4217  nnmsucr 4224  nnmcom 4225  oaabs 4236  2ecoptocl 4288  3ecoptocl 4289  th3qlem2 4299  xpdom1g 4424  supeq1 4549  supub 4554  suplub 4555  inf3lem2 4586  inf3lem5 4589  tz9.1 4618  r1pw 4658  cplem2 4693  karden 4698  aceq4 4706  aceq5lem5 4711  aceq6a 4713  aceq6b 4714  kmlem2 4738  kmlem13 4749  axrepnd 4918  axpowndlem3 4923  zfcndrep 4938  elnp 5064  prlem934a 5109  prlem934 5111  supexpr 5135  suppsr 5194  supsrlem6 5202  supre 5232  divmult 5676  divclt 5681  divcan1t 5689  divcan2t 5690  divrect 5702  divdirt 5713  divcan3t 5718  redivclt 5756  ltmul1t 5786  ltdiv1t 5805  ltmuldivt 5817  nn1suc 5887  nnaddclt 5888  nnmulclt 5889  nnleltp1t 5901  infm3 6001  infmsup 6015  xrsupsslem 6023  xrinfmsslem 6024  xrsupss 6025  xrinfmss 6026  uzind2 6154  uzindOLD 6156  uzwo4OLD 6158  zmax 6168  flval2t 6181  monoord 6231  om2uzlt 6235  seq1rn2 6258  ser1add2 6275  uzaddclt 6381  uzwo 6387  uzwoOLD 6388  nnwof 6391  indstr 6393  seqzrn2 6488  expcllem 6507  expeq0t 6517  expgt0t 6520  expgt1t 6523  mulexpt 6525  recexpt 6526  expaddt 6527  expmult 6528  expmwordit 6537  bernneq 6583  replimt 6692  cjexpt 6752  absdivt 6795  absexpt 6803  cjdivt 6827  seq1bnd 6847  cau3ir 6852  cvg2 6859  caubnd 6863  ser1absdiflem 6866  facdivt 6879  faclbnd 6882  faclbnd4lem4 6888  faclbnd6 6891  clim 6915  fsumconst 6976  bcxmas 7014  clm3 7017  clm4le 7019  clm0 7021  clmnns 7022  clm0nns 7023  clmi1 7024  clm4at 7028  clmi2at 7029  climfnn 7030  2climnn 7039  2climnn0 7040  climres 7042  iserzshft2 7044  climmulc2 7065  iserzex 7082  climubi 7089  climcau 7092  caucvglem1 7093  caucvg 7099  caucvg3t 7104  ser1cmp2 7113  cvgcmp3cetlem1 7124  cvgcmp3cetlem2 7125  expcnvlem5 7166  expcnv 7168  cvgratlem1ALT 7182  cvgratlem2ALT 7183  cvgratlem3ALT 7184  cvgratlem1 7185  cvgratlem3 7187  elcncf 7200  negfcncf 7204  rescncf 7207  ivthlem2 7217  ef0lem 7252  efaddlem27 7306  efexpt 7314  eftlext 7320  demoivre 7426  acdc3 7429  acdc5 7435  cnpfval 7697  ishaus 7722  metcnp2 7827  metcnpi 7829  metcnpi2 7830  metcni 7833  metcnp3 7835  metcnss 7837  cncfmet 7844  lmfval 7863  caufval 7864  lmbr 7866  lmbrf 7868  lmcvg 7870  iscau 7874  iscauf 7877  iscau5 7878  lmcvgnns 7879  lmss 7888  causs 7890  lmclim 7898  lmcau 7930  cncms 7932  bcthlem17 7949  bcthlem18 7950  ringid 8082  isnvlem 8167  isnvgOLD 8168  nvi 8173  va1cnlem 8279  sm1cnilem 8281  nmobndi 8370  nmounbi 8371  nmblolbi 8391  ipasslem1 8421  ipassi 8432  minveclem9 8484  minveclem24 8499  minveclem28 8503  spwmo 8580  axgroth3 8718  axgroth4 8719  h2hcau 8788  h2hlm 8789  hcau 8972  hcau2 8976  hlim 8977  hlim2 8981  hhcms 8993  hlimcaui 9027  hlimunii 9029  hhsscms 9067  occllem6 9094  projlem7 9108  projlem20 9121  projlem28 9129  projlem29 9130  pjthlem14 9147  pjtheut 9151  elspansn2t 9406  pjige0t 9553  pjcjt2 9554  pjopytht 9582  elcnopt 9700  elcnfnt 9726  cnopct 9753  cnfnct 9770  nmbdoplbt 9865  nmcoplbt 9875  lnfnmult 9892  nmbdfnlbt 9894  nmcfnlbt 9904  cnlnadjlem5 9919  pjss2co 10003  pjssmt 10004  stelt 10051  hstelt 10052  stcltr1 10111  mdbrt 10131  dmdbrt 10136  mddmd 10144  mdslmd1lem3 10162  mdslmd1lem4 10163  elat2 10175  atcvat2t 10224  cdj1 10265  ghomf1olem 10301  fveleq 10322  hmphre 10417  homcard 10426  fillsb 10435  filint2 10446  dtt2 10462  isded 10513  dedi 10514  iscat 10531  cati 10532  isfunb 10593

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