Theorem imbi1d 611

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

Hypothesis

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

Assertion

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

Proof of Theorem imbi1d

Step	Hyp	Ref	Expression
1		bid.1	. . . 4 |- (ph -> (ps <-> ch))
2	1	negbid 609	. . 3 |- (ph -> (-. ps <-> -. ch))
3	2	imbi2d 610	. 2 |- (ph -> ((-. th -> -. ps) <-> (-. th -> -. ch)))
4		pm4.1 164	. 2 |- ((ps -> th) <-> (-. th -> -. ps))
5		pm4.1 164	. 2 |- ((ch -> th) <-> (-. th -> -. ch))
6	3, 4, 5	3bitr4g 553	1 |- (ph -> ((ps -> th) <-> (ch -> th)))

Syntax hints:  -. wn 2   -> wi 3   <-> wb 146

This theorem is referenced by:  bibi2d 616  imbi1 621  imbi12d 624  pm5.33 648  con3th 764  drsb1 1171  ax11v2 1210  ax11inda 1364  rgen2a 1691  ralcom2 1768  raleq1f 1775  alexeq 1876  mo2icl 1914  sbcth2 1972  sbc19.21g 1977  ra4sbc 1987  r19.37zv 2341  ssuni 2512  intmin4 2549  trel 2677  ssexg 2711  dtruALT 2738  opth2 2789  pocl 2835  so 2855  onminex 3010  ordunisuc2 3105  dfom2 3123  findsg 3147  tfindsg 3152  tfindsg2 3153  vtoclr 3201  fun11 3548  funimass4 3748  f1fv 3859  caoprcan 4041  oaabs 4236  ertr 4258  ecoptocl 4287  ecopoprtrn 4295  dom2d 4385  unifi 4532  fiint 4534  supmo 4550  supub 4554  suplub 4555  suppr 4562  supsnALT 4564  karden 4698  aceq1 4701  zorn2lem1 4760  iscard2 4826  axrepndlem2 4917  axregndlem2 4927  indpi 5006  ltsopq 5047  prcdpq 5069  prlem934 5111  supexpr 5135  ltsosr 5175  suppsr 5194  supsrlem6 5202  supsr 5203  supre 5232  ltsor 5233  prodgt0 5775  prodgt0t 5782  prodge0t 5784  lbinfm 5995  infm3 6001  infmsup 6015  xrsupsslem 6023  xrinfmsslem 6024  supxr 6028  primet 6142  raluz 6374  fz1sbct 6449  sqrlem20 6622  abs3lemt 6844  seq1bnd 6847  cau2 6850  cau3i 6851  cau3ir 6852  cau5i 6854  cvg1 6858  cvg3 6860  cvganz 6861  clm3 7017  clm4 7018  climconst 7031  climshft 7041  climaddlem3 7052  climmullem8 7063  caucvglem2 7094  caucvglem5 7097  serzf0 7105  ser1f0 7106  ser1clim0 7109  cvgcmp3cetlem2 7125  cvgcmp3cet 7126  expcnvlem1 7162  expcnvlem6 7167  elcncf1d 7205  ivthlem6 7221  ivthlem7 7222  ivthlem6OLD 7230  ivthlem7OLD 7231  efaddlem25 7304  islp2 7688  cncnplem3 7715  metcnpi3 7831  metcnpi4 7832  metcni2 7834  cncfmet 7844  lmconst 7872  lmnn 7873  caun0 7880  metcld 7901  metcnp4 7904  xplm 7909  xpcn 7910  iscms2lem4 7926  isnvlem 8167  isnvgOLD 8168  nvi 8173  nmcnilem 8272  va1cnlem 8279  sm1cnilem 8281  blocni 8396  spwval2 8577  efifolem3 8639  norm3lemt 8940  chlim 9025  hlim0 9026  projlem20 9121  pjth 9148  omlsi 9160  eigortht 9681  0cnop 9819  0cnfn 9820  idcnop 9821  lnopcon 9878  lnfncon 9905  nlelch 9909  stcltr1 10111  elat2 10175  ghomf1olem 10301  fillsb 10435  isded 10513  dedi 10514  iscat 10531  cati 10532  ismona 10579  ismonb 10580  imonclem 10583

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