Theorem imbi1i 325

Description: Introduce a consequent to both sides of a logical equivalence. (Contributed by NM, 3-Jan-1993.) (Proof shortened by Wolf Lammen, 17-Sep-2013.)

Hypothesis

Ref	Expression
imbi1i.1

Assertion

Ref	Expression
imbi1i

Proof of Theorem imbi1i

Step	Hyp	Ref	Expression
1		imbi1i.1	. 2
2		imbi1 323	. 2
3	1, 2	ax-mp 5	1

Syntax hints:  ->wi 4  <->wb 184

This theorem is referenced by:  imor  412  ancomst  452  ifpn  1391  eximal  1615  19.43  1693  19.37v  1768  19.37  1966  dfsb3  2115  sbrim  2137  sbor  2139  mo4f  2336  2mos  2375  neor  2781  r3al  2837  r3alOLD  2895  r19.23t  2935  r19.23v  2937  r19.43  3013  ceqsralt  3133  ralab  3260  ralrab  3261  euind  3286  reu2  3287  rmo4  3292  reuind  3303  2reu5lem3  3307  rmo3  3429  raldifb  3643  unss  3677  ralunb  3684  inssdif0  3895  ssundif  3911  dfif2  3943  pwss  4027  ralsnsg  4061  disjsn  4090  snss  4154  raldifsni  4160  raldifsnb  4161  unissb  4281  intun  4319  intpr  4320  dfiin2g  4363  disjor  4436  dftr2  4547  axrep1  4564  axpweq  4629  zfpow  4631  axpow2  4632  reusv2lem4  4656  reusv2  4658  reusv7OLD  4664  raliunxp  5147  asymref2  5389  dffun2  5603  dffun4  5605  dffun5  5606  dffun7  5619  fununi  5659  fvn0ssdmfun  6022  dff13  6166  dff14b  6178  zfun  6593  uniex2  6595  dfom2  6702  fimaxg  7787  fiint  7817  dfsup2  7922  oemapso  8122  scottexs  8326  scott0s  8327  iscard2  8378  acnnum  8454  dfac9  8537  dfacacn  8542  kmlem4  8554  kmlem12  8562  axpowndlem3  8996  axpowndlem3OLD  8997  zfcndun  9014  zfcndpow  9015  zfcndac  9018  axgroth5  9223  grothpw  9225  axgroth6  9227  addsrmo  9471  mulsrmo  9472  infm3  10527  raluz2  11159  nnwos  11178  ralrp  11267  lo1resb  13387  rlimresb  13388  o1resb  13389  modfsummod  13608  isprm4  14227  acsfn1  15058  acsfn2  15060  lublecllem  15618  isirred2  17350  isdomn2  17948  iunocv  18712  ist1-2  19848  isnrm2  19859  dfcon2  19920  alexsubALTlem3  20549  ismbl  21937  dyadmbllem  22008  ellimc3  22283  dchrelbas2  23512  dchrelbas3  23513  isch2  26141  choc0  26244  h1dei  26468  mdsl2i  27241  rmo3f  27394  rmo4fOLD  27395  rmo4f  27396  disjorf  27440  axextprim  29073  axunprim  29075  axpowprim  29076  untuni  29081  3orit  29092  biimpexp  29093  dfon2lem8  29222  predreseq  29259  soseq  29334  dfom5b  29562  wl-equsalcom  29995  tsim1  30537  fphpd  30750  dford4  30971  fnwe2lem2  30997  isdomn3  31164  pm14.12  31328  fsummulc1f  31569  dvmptmulf  31734  dvnmul  31740  dvmptfprodlem  31741  dvnprodlem2  31744  aacllem  33216  dfvd2an  33359  dfvd3  33368  dfvd3an  33371  uun2221  33610  uun2221p1  33611  uun2221p2  33612  bnj538OLD  33797  bnj1101  33843  bnj1109  33845  bnj1533  33910  bnj580  33971  bnj864  33980  bnj865  33981  bnj978  34007  bnj1049  34030  bnj1090  34035  bnj1145  34049  bj-axrep1  34374  bj-zfpow  34381  cvlsupr3  35069  pmapglbx  35493  isltrn2N  35844  cdlemefrs29bpre0  36122  bj-ifidg  37707  bj-ifid1g  37708  bj-ifor123g  37725  elintima  37765  cotr2g  37786  dfhe3  37799

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 185