Theorem imbi2d 615

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

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

This theorem is referenced by:  imbi1d 616  orbi2d 617  bibi2d 621  imbi12d 629  pm5.42 655  dedlem0a 765  con3th 771  19.23t 1152  ax11v2 1252  sbcom 1296  sbcom2 1373  ax15 1398  ax11eq 1402  ax11el 1403  ax11indalem 1407  ax11inda2ALT 1408  ax11inda 1410  mo 1432  2mo 1487  2eu6 1494  ralcom2 1822  2gencl 1875  3gencl 1876  vtocl2gf 1895  vtocl2ga 1899  vtocl3ga 1900  mo2icl 1969  reu7 1981  sbc5g 1999  sbc6g 2000  sbcel1gv 2028  sbcel2gv 2029  uniiunlem 2184  r19.36zv 2408  dedth2h 2441  dedth3h 2442  dedth4h 2443  elint 2606  elinti 2609  elintrabg 2613  intab 2627  trel 2761  trss 2763  axrep1 2768  axrep2 2769  axrep3 2770  bm1.3ii 2780  opthgg 2865  pocl 2922  solin 2936  freq1 2952  reuuni2f 3107  tfindsg 3213  tfinds2 3216  tfinds3 3217  dfom2 3220  elom 3221  elomg 3222  findsg 3245  finds2 3246  vtoclr 3294  2optocl 3322  3optocl 3323  resieq 3463  funimaexg 3681  funopfvg 3863  fnbrfvb 3864  funbrfvbg 3868  fvelima 3875  fnressn 3951  fressnfv 3952  f1fveq 3990  ndmoprcl 4105  caoprcan 4116  caoprord 4117  tfrlem1 4212  tfr3 4227  oaordi 4316  oeordi 4350  oeoa 4360  oeoe 4362  nnacl 4369  nnmcl 4370  nnecl 4371  nnacom 4373  nnmsucr 4380  nnmcom 4381  oaabs 4392  2ecoptocl 4445  3ecoptocl 4446  th3qlem2 4456  xpdom1g 4585  supeq1 4718  supub 4723  suplub 4724  inf3lem2 4759  inf3lem5 4762  tz9.1 4792  r1pw 4832  cplem2 4867  karden 4872  aceq4 4880  aceq5lem5 4885  aceq6a 4887  aceq6b 4888  kmlem2 4912  kmlem13 4923  cdaeng 5076  axrepnd 5100  axpowndlem3 5105  zfcndrep 5120  elnp 5246  prlem934a 5291  prlem934 5293  supexpr 5317  suppsr 5376  supsrlem6 5384  supre 5414  divmul 5859  divcl 5864  divcan1 5872  divrec 5885  divdir 5896  divcan3 5901  redivcl 5940  ltmul1 5970  ltdiv1 5993  ltdiv1OLD 5994  ltmuldiv 6007  ltmuldivOLD 6008  nn1suc 6084  nnaddcl 6085  nnmulcl 6086  nnleltp1 6100  infm3 6222  infmsup 6236  xrsupsslem 6244  xrinfmsslem 6245  xrsupss 6246  xrinfmss 6247  uzind2 6377  uzindOLD 6379  uzwo4OLD 6381  zindd 6386  zmax 6392  flval2 6437  monoord 6482  uzaddcl 6576  uzwo 6582  uzwoOLD 6583  nnwof 6586  indstr 6588  om2uzlti 6661  seq1rn2 6686  ser1add2i 6703  seqzrn2 6751  expcllem 6770  expeq0 6780  expgt0 6783  expgt1 6786  mulexp 6788  exprec 6789  exprecOLD 6790  expadd 6791  expmul 6792  expmwordi 6803  bernneq 6849  bernneqOLD 6850  replim 6962  cjexp 7018  absdiv 7062  absexp 7070  cjdiv 7092  seq1bndi 7113  cau3iri 7118  cvg2i 7125  caubndi 7129  ser1absdiflem 7132  facdiv 7145  faclbnd 7148  faclbnd4lem4 7154  faclbnd6 7157  clim 7180  fsumconst 7241  bcxmas 7279  clm3i 7282  clm4lei 7284  clm0i 7286  clmnnsi 7287  clm0nnsi 7288  clmi1i 7289  clm4a 7293  clmi2a 7294  climfnn 7295  2climnn 7305  2climnn0 7306  climresi 7308  iserzshft2i 7310  climabs0i 7316  climmulc2 7332  iserzexi 7349  climubii 7356  climcaui 7359  caucvglem1 7360  caucvgi 7366  caucvg3 7371  ser1cmp2i 7380  cvgcmp3cetlem1 7392  cvgcmp3cetlem2 7393  expcnvlem5 7435  expcnv 7437  cvgratlem1ALT 7452  cvgratlem2ALT 7453  cvgratlem3ALT 7454  cvgratlem1 7455  cvgratlem3 7457  elcncf 7470  negfcncfi 7474  rescncf 7477  ivthlem2 7487  ef0lem 7515  efaddlem27 7569  efexp 7577  eftlex 7583  demoivre 7695  acdc3 7698  acdc5 7705  cnpfval 7967  iscnp2 7971  ishaus 7993  metcnp2 8099  metcnpi 8101  metcnpi2 8102  metcni 8105  metcnp3 8107  metcnss 8109  cncfmet 8116  lmfval 8136  caufval 8137  lmbr 8139  lmbrf 8141  lmcvg 8143  iscau 8147  iscauf 8150  iscau5 8152  lmbrnns 8153  lmcvgnns 8154  iscaunns 8155  lmss 8164  causs 8166  lmclim 8174  lmcau 8207  cncms 8209  bcthlem17 8226  bcthlem18 8227  gxnn0suc 8320  gxnn0add 8330  gxnn0mul 8333  ringid 8386  isnvlem 8476  nvi 8480  vacnlem3 8584  va1cnlem 8599  sm1cnilem 8601  nmobndi 8692  nmounbi 8693  nmblolbi 8715  ipasslem1 8746  ipassi 8757  minveclem9 8813  minveclem24 8828  minveclem28 8832  spwmo 8918  spwpr4 8925  spwpr4OLD 8926  spwpr4aOLD 8927  axgroth3 9051  axgroth4 9052  h2hcau 9124  h2hlm 9125  hcau 9327  hcau2 9331  hlimi 9332  hlim2 9336  hhcms 9348  hlimcauii 9382  hlimuniii 9384  hhsscms 9426  occllem6 9454  projlem7 9468  projlem20 9481  projlem28 9489  projlem29 9490  pjthlem14 9508  pjtheu 9512  elspansn2 9766  pjige0 9914  pjcjt2 9915  pjopyth 9943  elcnop 10063  elcnfn 10089  cnopc 10117  cnfnc 10134  nmbdoplb 10229  nmcoplb 10239  lnfnmul 10256  nmbdfnlb 10258  nmcfnlb 10268  cnlnadjlem5 10283  pjss2coi 10372  pjssmi 10373  stel 10422  hstel 10423  stcltr1i 10482  mdbr 10502  dmdbr 10507  mddmd2 10517  mdslmd1lem3 10535  mdslmd1lem4 10536  elat2 10548  atcvat2 10598  cdj1i 10642  ghomf1olem 10681  fveleq 10700  domleqt 10792  inposet 10868  dupos1 10876  on1el3 10962  on1el4 10963  hmphre 11036  homcard 11045  issubsplem1 11058  issubspt 11059  fillsb 11073  filint2 11084  limfillem2 11102  dtt2 11110  isded 11190  dedi 11191  iscat 11208  cati 11209  isfunb 11289  isplig 11319  eqeu 11394  fictb 11423  finsschain 11425  ordtypelem5 11431  ordtypelem6 11432  elomsubsd 11446  hausnei2 11471  connsub 11502  2ndc1stc 11538  neibastop2lem1 11580  neibastop2lem4 11583  ist0 11599  isreg 11609  isnrm 11612  ufileulem 11657  ufileu 11658  fbaslim 11680  limfilcf 11683  rnelfm 11699  isflimf 11709  flimfbas 11713  fclusbas 11722  fcluscf 11724  fcluscomplem 11732  isfclusf 11737  gagrpid 11780  gaass 11781  erthdmg 11824  dif1en 11833  fixp 11840  supubt 11855  eluzadd 11860  sdclem1 11875  sdclem2 11876  seqpo 11878  incsequz 11879  fsumltisum 11887  fsumleisum 11890  mettrifi2 11913  lmclim2 11915  caushft 11916  caures 11917  lmtlm 11969  heiborlem16 12026  heiborlem34 12044  heiborlem35 12045  rrncms 12075

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 145  df-an 223

Copyright terms: Public domain