Theorem imbi1d 308

Description: Deduction adding a consequent to both sides of a logical equivalence. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 17-Sep-2013.)

Hypothesis

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

Assertion

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

Proof of Theorem imbi1d

Step	Hyp	Ref	Expression
1		imbid.1	. . . 4 |- (ph -> (ps <-> ch))
2	1	biimprd 214	. . 3 |- (ph -> (ch -> ps))
3	2	imim1d 69	. 2 |- (ph -> ((ps -> th) -> (ch -> th)))
4	1	biimpd 198	. . 3 |- (ph -> (ps -> ch))
5	4	imim1d 69	. 2 |- (ph -> ((ch -> th) -> (ps -> th)))
6	3, 5	impbid 183	1 |- (ph -> ((ps -> th) <-> (ch -> th)))

Syntax hints:   -> wi 4   <-> wb 176

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

This theorem depends on definitions:  df-bi 177

This theorem is referenced by:  imbi12d  311  imbi1  313  imim21b  356  pm5.33  848  con3th  924  ax12bOLD  1690  19.21t  1795  ax11v2  1992  drsb1  2022  ax11vALT  2097  ax11inda  2200  ax11v2-o  2201  ralcom2  2776  raleqf  2804  alexeq  2969  mo2icl  3016  sbc19.21g  3111  csbiebg  3176  ralss  3333  r19.37zv  3647  ssuni  3914  intmin4  3956  eqpw1uni  4331  nnsucelr  4429  nndisjeq  4430  preaddccan2lem1  4455  preaddccan2  4456  leltfintr  4459  ssfin  4471  ncfinlower  4484  sfinltfin  4536  spfinsfincl  4540  vfinspss  4552  vtoclr  4817  fun11  5160  funimass4  5369  dff13  5472  oprabid  5551  caovcan  5629  clos1conn  5880  trd  5922  frd  5923  extd  5924  antird  5929  antid  5930  ecoptocl  5997  enprmapc  6084  nclenn  6250  addccan2nc  6266  nchoicelem12  6301  nchoicelem16  6305  nchoicelem17  6306  fnfrec  6321