Theorem imbi2i 202

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	biimpi 168	. . 3 |- (ph -> ps)
3	2	imim2i 11	. 2 |- ((ch -> ph) -> (ch -> ps))
4	1	biimpri 169	. . 3 |- (ps -> ph)
5	4	imim2i 11	. 2 |- ((ch -> ps) -> (ch -> ph))
6	3, 5	impbii 174	1 |- ((ch -> ph) <-> (ch -> ps))

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

This theorem is referenced by:  imbi12i 205  iman 256  orbi2i 275  or12 278  pm4.14 379  pm4.15 380  pm4.78 381  pm4.79 382  anidmdbi 481  anass 487  ibibr 651  bibi2i 669  bibi2iOLD 670  pm5.32 706  pm5.6 752  nan 753  impexp3a 1292  19.35 1426  19.36 1429  sban 1607  sbhb 1714  2sb6 1726  2sb6rf 1729  eu1 1786  sbmo 1796  moabs 1811  moanim 1826  2eu6 1858  r2al 2136  r19.21t 2177  r19.35 2231  ralcom2 2244  ralcom2OLD 2245  reu2 2442  reu8 2448  ssconb 2738  ssin 2814  difin 2831  reldisj 2916  reldisjOLD 2917  inssdif0OLD 2941  ssundif 2955  pwpw0 3134  pwsnALT 3173  unissb 3208  dfiin2OLD 3288  ssiunOLD 3294  ssiin 3302  ssiinOLD 3303  axrep1 3429  dffr2 3627  dffr2OLD 3628  dfepfr 3640  dfepfrOLD 3641  ssrel 4075  dffr3 4297  asymref2OLD 4311  fun11 4480  dff13 4850  ordtypelem7 5690  inf2 5714  axinf2 5730  aceq1 5891  aceq0 5892  zfac 5907  ac6n 5919  kmlem14 5940  aceqkm 5943  zfcndrep 6118  zfcndac 6123  prime 7407  raluz2 7612  cau3iri 8167  clm1i 8337  climshfti 8364  climresi 8365  caucvgi 8423  islp2 9023  sncld 9064  lmbr2 9207  iscau2 9215  metcnp4 9248  bcthlem7 9283  nmobndseqi 9780  axgroth6 10137  axgroth4 10139  grothprim 10141  hausfillim 10303  cvnbtwn3 11860  elat2 11912  bnj24 12388  bnj37 12407  bnj47OLD 12418  bnj48OLD 12423  bnj55 12430  bnj220 12511  bnj614 12567  bnj856 12789  bnj859 12792  bnj861 12794  bnj877 12804  bnj901 12818  bnj979 12863  bnj997 12873  bnj1054 12891  bnj1059 12896  bnj1085 12907  bnj1086 12908  bnj1088 12910  bnj1130 12933  bnj1135 12935  bnj1166 12958  bnj1306 13049  bnj1310 13050  bnj1492 13161  bnj1533 13182  bnj119 13229  bnj121 13231  bnj124 13234  bnj130 13240  bnj153 13247  bnj207 13248  bnj611 13307  bnj965 13346  bnj1000 13364  bnj1008 13373  bnj1021 13380  bnj1047 13393  bnj1049 13394  bnj1062 13397  bnj1067 13399  bnj1070 13401  bnj1077 13405  bnj1090 13410  bnj1171 13439  bnj1172 13440  bnj1174 13442  bnj1284 13482  isprm2 13775  axinfprim 13790  dfon2lem9 13857  dffr4 13893  df3nandALT1 14146  df3nandALT2 14147  evpexun 14322  elicc3 15362  ordtypelem7OLD 15381  alexsublem3 15439  is1stc3 15469  neibastop2lem3 15521  ist0-2 15539  limfilcf 15587  flimfnfcls 15615  sbmoOLD 15654  caures 15852  pm10.541 16314  pm13.196a 16378

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 164

Copyright terms: Public domain