Theorem imbi1i 315

Description: Introduce 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
imbi1i.1	|- (ph <-> ps)

Assertion

Ref	Expression
imbi1i	|- ((ph -> ch) <-> (ps -> ch))

Proof of Theorem imbi1i

Step	Hyp	Ref	Expression
1		imbi1i.1	. 2 |- (ph <-> ps)
2		imbi1 313	. 2 |- ((ph <-> ps) -> ((ph -> ch) <-> (ps -> ch)))
3	1, 2	ax-mp 5	1 |- ((ph -> ch) <-> (ps -> ch))

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:  imbi12i  316  imor  401  ancomsimp  1369  19.43  1605  19.37  1873  dfsb3  2056  sbor  2066  sbrim  2067  mo4f  2236  2mos  2283  neor  2601  r3al  2672  r19.23t  2729  r19.43  2767  ceqsralt  2883  ralab  2998  ralrab  2999  euind  3024  reu2  3025  rmo4  3030  reuind  3040  2reu5lem3  3044  rmo3  3134  unss  3438  ralunb  3445  inssdif0  3618  ssundif  3634  dfif2  3665  pwss  3737  ralsns  3764  disjsn  3787  snss  3839  unissb  3922  intun  3959  intpr  3960  dfiin2g  4001  eqpw1  4163  pw111  4171  ssrelk  4212  eqrelk  4213  elp6  4264  sikexlem  4296  insklem  4305  peano5  4410  ltfintrilem1  4466  evenodddisjlem1  4516  nnadjoin  4521  nnpweq  4524  raliunxp  4824  intirr  5030  dffun4  5122  dffun5  5123  dffun7  5134  fun11  5160  fununi  5161  dff13  5472  clos1induct  5881  dfnnc3  5886  enmap2lem4  6067  enmap1lem4  6073  spacind  6288