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  2775  raleqf  2803  alexeq  2968  mo2icl  3015  sbc19.21g  3110  csbiebg  3175  ralss  3332  r19.37zv  3646  ssuni  3913  intmin4  3955  eqpw1uni  4330  nnsucelr  4428  nndisjeq  4429  preaddccan2lem1  4454  preaddccan2  4455  leltfintr  4458  ssfin  4470  ncfinlower  4483  sfinltfin  4535  spfinsfincl  4539  vfinspss  4551  vtoclr  4816  fun11  5159  funimass4  5368  dff13  5471  oprabid  5550  caovcan  5628  clos1conn  5879  trd  5921  frd  5922  extd  5923  antird  5928  antid  5929  ecoptocl  5996  enprmapc  6083  nclenn  6249  addccan2nc  6265  nchoicelem12  6300  nchoicelem16  6304  nchoicelem17  6305  fnfrec  6320