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 589  bibi2i 606  pm5.32 642  pm5.6 686  nan 687  nicodraw 949  19.35 1071  19.36 1074  sban 1232  2sb6 1331  2sb6rf 1334  eu1 1385  moabs 1408  moanim 1420  2eu6 1447  r2al 1668  r19.21t 1707  r19.35 1751  ralcom2 1768  reu2 1920  reu8 1926  ssconb 2160  reldisj 2303  inssdif0 2323  ssundif 2334  pwpw0 2460  unissb 2518  dfiin2 2578  ssiun 2582  ssiin 2589  axrep1 2684  dffr2 2909  dfepfr 2922  dffr3 3415  asymref2 3424  asymref2OLD 3426  fun11 3548  f1fv 3859  inf2 4580  axinf2 4596  aceq1 4701  aceq0 4702  axac 4717  ac6n 4729  kmlem14 4750  aceqkm 4753  zfcndrep 4938  zfcndac 4943  primet 6142  raluz2 6375  cau3ir 6852  clm1 7015  climshft 7041  climres 7042  caucvg 7099  islp2 7688  sncld 7726  lmbr2 7867  iscau2 7875  metcnp4 7904  bcthlem7 7939  nmobndseqi 8372  axgroth4 8719  grothprim 8722  cvnbtwn3t 10125  elat2 10175  anidmdbi 10334

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