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 763  drsb1 1158  ax11v2 1199  ax11inda 1348  rgen2a 1675  ralcom2 1752  raleq1f 1759  alexeq 1857  mo2icl 1895  sbcth2 1953  sbc19.21g 1958  ra4sbc 1968  r19.37zv 2322  ssuni 2490  intmin4 2527  trel 2655  ssexg 2689  dtruALT 2716  opth2 2765  pocl 2808  so 2828  onminex 2983  ordunisuc2 3078  dfom2 3096  findsg 3120  tfindsg 3125  tfindsg2 3126  vtoclr 3173  fun11 3502  funimass4 3702  f1fv 3813  caoprcan 3995  oaabs 4190  ertr 4212  ecoptocl 4241  ecopoprtrn 4249  dom2d 4339  unifi 4484  fiint 4486  supmo 4502  supub 4506  suplub 4507  suppr 4514  supsnALT 4516  karden 4650  aceq1 4653  zorn2lem1 4712  iscard2 4777  axrepndlem2 4868  axregndlem2 4878  indpi 4957  ltsopq 4998  prcdpq 5020  prlem934 5062  supexpr 5086  ltsosr 5126  suppsr 5145  supsrlem6 5153  supsr 5154  supre 5183  ltsor 5184  prodgt0 5726  prodgt0t 5733  prodge0t 5735  lbinfm 5946  infm3 5952  infmsup 5966  xrsupsslem 5974  xrinfmsslem 5975  supxr 5979  primet 6093  raluz 6325  fz1sbct 6400  sqrlem20 6573  abs3lemt 6795  seq1bnd 6798  cau2 6801  cau3i 6802  cau3ir 6803  cau5i 6805  cvg1 6809  cvg3 6811  cvganz 6812  clm3 6968  clm4 6969  climconst 6982  climshft 6992  climaddlem3 7003  climmullem8 7014  caucvglem2 7045  caucvglem5 7048  serzf0 7056  ser1f0 7057  ser1clim0 7060  cvgcmp3cetlem2 7076  cvgcmp3cet 7077  expcnvlem1 7113  expcnvlem6 7118  elcncf1d 7156  ivthlem6 7172  ivthlem7 7173  ivthlem6OLD 7181  ivthlem7OLD 7182  efaddlem25 7255  islp2 7636  cncnplem3 7663  metcnpi3 7779  metcnpi4 7780  metcni2 7782  cncfmet 7792  lmconst 7820  lmnn 7821  caun0 7828  metcld 7849  metcnp4 7852  xplm 7857  xpcn 7858  iscms2lem4 7874  isnvg 8109  nvi 8111  nmcnilem 8209  va1cnlem 8214  sm1cnilem 8216  blocni 8331  efifolem3 8552  ghomf1olem 8663  fillsb 8785  isded 8863  dedi 8864  iscat 8881  cati 8882  ismona 8929  ismonb 8930  imonclem 8933  norm3lemt 9168  chlim 9255  hlim0 9256  projlem20 9335  pjth 9362  omlsi 9374  eigortht 9895  0cnop 10033  0cnfn 10034  idcnop 10035  lnopcon 10092  lnfncon 10119  nlelch 10123  stcltr1 10325  elat2 10389

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