Theorem imbi1d 613

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 611	. . 3 |- (ph -> (-. ps <-> -. ch))
3	2	imbi2d 612	. 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 555	1 |- (ph -> ((ps -> th) <-> (ch -> th)))

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

This theorem is referenced by:  bibi2d 618  imbi1 623  imbi12d 626  pm5.33 650  con3th 766  drsb1 1175  ax11v2 1215  ax11inda 1371  rgen2a 1699  ralcom2 1776  raleq1f 1783  alexeq 1885  mo2icl 1923  sbcth2 1982  sbc19.21g 1987  ra4sbc 1997  r19.37zv 2351  ssuni 2522  intmin4 2559  trel 2687  ssexg 2721  dtruALT 2748  opth2 2800  pocl 2844  so 2864  onminex 3020  ordunisuc2 3115  dfom2 3133  findsg 3157  tfindsg 3162  tfindsg2 3163  vtoclr 3211  fun11 3562  funimass4 3763  f1fv 3874  caoprcan 4055  oaabs 4252  ertr 4274  ecoptocl 4303  ecopoprtrn 4311  dom2d 4404  unifiOLD 4557  fiint 4559  fiintOLD 4560  supmo 4576  supub 4580  suplub 4581  supmaxlem 4588  suppr 4590  supsnALT 4592  karden 4726  aceq1 4729  zorn2lem1 4788  iscard2 4854  axrepndlem2 4945  axregndlem2 4955  indpi 5034  ltsopq 5075  prcdpq 5097  prlem934 5139  supexpr 5163  ltsosr 5203  suppsr 5222  supsrlem6 5230  supsr 5231  supre 5260  ltsor 5261  prodgt0 5819  prodgt0t 5826  prodge0t 5828  lbinfm 6048  infm3 6054  infmsup 6068  xrsupsslem 6076  xrinfmsslem 6077  supxr 6081  primet 6195  raluz 6442  fz1sbct 6517  sqrlem20 6692  abs3lemt 6907  seq1bnd 6910  cau2 6913  cau3i 6914  cau3ir 6915  cau5i 6917  cvg1 6921  cvg3 6923  cvganz 6924  clm3 7079  clm4 7080  climconst 7094  climshft 7104  climaddlem3 7116  climmullem8 7127  caucvglem2 7158  caucvglem5 7161  serzf0 7169  ser1f0 7170  ser1clim0 7173  cvgcmp3cetlem2 7189  cvgcmp3cet 7190  expcnvlem1 7227  expcnvlem6 7232  elcncf1d 7270  ivthlem6 7286  ivthlem7 7287  efaddlem25 7362  islp2 7747  cncnplem3 7776  metcnpi3 7892  metcnpi4 7893  metcni2 7895  cncfmet 7905  lmconst 7934  lmnn 7935  caun0 7945  metcld 7967  metcnp4 7970  xplm 7975  xpcn 7976  iscms2lem4 7992  isnvlem 8229  nvi 8233  nmcnilem 8337  va1cnlem 8345  sm1cnilem 8347  blocni 8465  spwval2 8653  spwpr2 8658  efifolem3 8724  norm3lemt 9019  chlim 9104  hlim0 9105  projlem20 9205  pjth 9233  omlsi 9245  eigortht 9764  0cnop 9903  0cnfn 9904  idcnop 9905  lnopcon 9963  lnfncon 9990  nlelch 9994  stcltr1 10201  elat2 10267  ghomf1olem 10396  fillsb 10560  isded 10669  dedi 10670  iscat 10687  cati 10688  ismona 10737  ismonb 10738  imonclem 10741  isepia 10747  isepib 10748

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