Theorem imbi2i 185

Description: Introduce an antecedent to both sides of a logical equivalence.

Hypothesis

Ref	Expression
bi.a	|- (ph <-> ps)

Assertion

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

Proof of Theorem imbi2i

Step	Hyp	Ref	Expression
1		bi.a	. . . 4 |- (ph <-> ps)
2	1	biimp 151	. . 3 |- (ph -> ps)
3	2	imim2i 17	. 2 |- ((ch -> ph) -> (ch -> ps))
4	1	biimpr 152	. . 3 |- (ps -> ph)
5	4	imim2i 17	. 2 |- ((ch -> ps) -> (ch -> ph))
6	3, 5	impbi 157	1 |- ((ch -> ph) <-> (ch -> ps))

Syntax hints:   -> wi 3   <-> wb 146

This theorem is referenced by:  imbi12i 188  iman 237  orbi2i 255  or12 258  pm4.14 352  pm4.15 353  pm4.78 354  pm4.79 355  anass 439  ibibr 591  bibi2i 608  pm5.32 644  pm5.6 688  nan 689  nicodraw 952  19.35 1075  19.36 1078  sban 1237  2sb6 1336  2sb6rf 1339  eu1 1392  moabs 1415  moanim 1427  2eu6 1454  r2al 1676  r19.21t 1715  r19.35 1759  ralcom2 1776  reu2 1930  reu8 1936  ssconb 2170  reldisj 2313  inssdif0 2333  ssundif 2344  pwpw0 2469  pwsnALT 2501  unissb 2528  dfiin2 2588  ssiun 2592  ssiin 2599  axrep1 2694  dffr2 2919  dfepfr 2932  dffr3 3431  asymref2 3440  fun11 3562  f1fv 3874  inf2 4608  axinf2 4624  aceq1 4729  aceq0 4730  axac 4745  ac6n 4757  kmlem14 4778  aceqkm 4781  zfcndrep 4966  zfcndac 4971  primet 6195  raluz2 6443  cau3ir 6915  clm1 7077  climshft 7104  climres 7105  caucvg 7163  islp2 7747  sncld 7787  lmbr2 7929  iscau2 7937  metcnp4 7970  bcthlem7 8005  nmobndseqi 8440  axgroth4 8780  grothprim 8783  cvnbtwn3t 10215  elat2 10267  anidmdbi 10434

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

Copyright terms: Public domain