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 4403  unifi 4550  fiint 4552  supmo 4568  supub 4572  suplub 4573  supmaxlem 4580  suppr 4582  supsnALT 4584  karden 4718  aceq1 4721  zorn2lem1 4780  iscard2 4846  axrepndlem2 4937  axregndlem2 4947  indpi 5026  ltsopq 5067  prcdpq 5089  prlem934 5131  supexpr 5155  ltsosr 5195  suppsr 5214  supsrlem6 5222  supsr 5223  supre 5252  ltsor 5253  prodgt0 5807  prodgt0t 5814  prodge0t 5816  lbinfm 6036  infm3 6042  infmsup 6056  xrsupsslem 6064  xrinfmsslem 6065  supxr 6069  primet 6183  raluz 6428  fz1sbct 6503  sqrlem20 6678  abs3lemt 6892  seq1bnd 6895  cau2 6898  cau3i 6899  cau3ir 6900  cau5i 6902  cvg1 6906  cvg3 6908  cvganz 6909  clm3 7064  clm4 7065  climconst 7079  climshft 7089  climaddlem3 7101  climmullem8 7112  caucvglem2 7143  caucvglem5 7146  serzf0 7154  ser1f0 7155  ser1clim0 7158  cvgcmp3cetlem2 7174  cvgcmp3cet 7175  expcnvlem1 7212  expcnvlem6 7217  elcncf1d 7255  ivthlem6 7271  ivthlem7 7272  efaddlem25 7347  islp2 7732  cncnplem3 7761  metcnpi3 7877  metcnpi4 7878  metcni2 7880  cncfmet 7890  lmconst 7919  lmnn 7920  caun0 7930  metcld 7952  metcnp4 7955  xplm 7960  xpcn 7961  iscms2lem4 7977  isnvlem 8214  nvi 8218  nmcnilem 8322  va1cnlem 8330  sm1cnilem 8332  blocni 8450  spwval2 8638  spwpr2 8643  efifolem3 8709  norm3lemt 9004  chlim 9089  hlim0 9090  projlem20 9190  pjth 9218  omlsi 9230  eigortht 9749  0cnop 9888  0cnfn 9889  idcnop 9890  lnopcon 9948  lnfncon 9975  nlelch 9979  stcltr1 10186  elat2 10252  ghomf1olem 10381  fillsb 10520  isded 10612  dedi 10613  iscat 10630  cati 10631  ismona 10678  ismonb 10679  imonclem 10682

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