Theorem imbi1d 465

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 463	. . 3 |- (ph -> (-. ps <-> -. ch))
3	2	imbi2d 464	. 2 |- (ph -> ((-. th -> -. ps) <-> (-. th -> -. ch)))
4		pm4.1 143	. 2 |- ((ps -> th) <-> (-. th -> -. ps))
5		pm4.1 143	. 2 |- ((ch -> th) <-> (-. th -> -. ch))
6	3, 4, 5	3bitr4g 428	1 |- (ph -> ((ps -> th) <-> (ch -> th)))

Syntax hints:  -. wn 1   -> wi 2   <-> wb 127

This theorem is referenced by:  bibi2d 470  imbi1 472  imbi12d 474  elimant 505  con3th 573  rgen2 1248  ralcom2 1314  raleqf 1321  alexeq 1409  mo2icl 1434  sbc19.21g 1470  rax4 1471  ssexg 1702  opth2 1909  ssuni 1937  trel 2048  pocl 2132  so 2152  supmo 2156  supub 2160  suplub 2161  supsn 2168  onminex 2275  dfom2 2374  findsg 2398  tfindsg 2402  tfindsg2 2403  vtoclr 2449  f1fv 2916  caoprcan 3069  ertr 3211  ecoptocl 3239  ecopoprtrn 3247  dom2d 3307  fiint 3445  karden 3551  aceq1 3552  zornlem1 3603  iscard2 3660  axrepndlem2 3739  axregndlem2 3749  indpi 3828  ltsopq 3869  prcdpq 3891  prlem934 3933  suppr 3957  ltsosr 3997  suppsr 4016  supsrlem6 4024  supsr 4025  supre 4054  ltsor 4055  prodgt0 4388  sqrlem20 4750  abs3lemt 4865  clim0 4882  norm3lemt 5097  chlim 5139  hlim0 5140  projlem20 5212  pjth 5239  omlsi 5250  stcltr1 5707  elat2 5739

This theorem was proved from axioms:  ax-1 3  ax-2 4  ax-3 5  ax-mp 6

This theorem depends on definitions:  df-bi 128  df-an 198

metamath.org