Theorem imbi12i 326

Description: Join two logical equivalences to form equivalence of implications. (Contributed by NM, 1-Aug-1993.)

Hypotheses

Ref	Expression
imbi12i.1
imbi12i.2

Assertion

Ref	Expression
imbi12i

Proof of Theorem imbi12i

Step	Hyp	Ref	Expression
1		imbi12i.1	. 2
2		imbi12i.2	. 2
3		imbi12 322	. 2
4	1, 2, 3	mp2 9	1

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

This theorem is referenced by:  orimdi  847  nanbi  1352  rb-bijust  1582  nfbii  1644  sbnf2  2183  sb8mo  2320  cbvmo  2322  raleqbii  2902  rmo5  3076  cbvrmo  3083  ss2ab  3567  sbcssg  3940  trint  4560  ssextss  4706  relop  5158  dmcosseq  5269  cotrg  5383  issref  5385  cnvsym  5386  intasym  5387  intirr  5390  codir  5392  qfto  5393  cnvpo  5550  dff14a  6177  porpss  6584  funcnvuni  6753  poxp  6912  cp  8330  aceq2  8521  kmlem12  8562  kmlem15  8565  zfcndpow  9015  grothprim  9233  dfinfmr  10545  infmsup  10546  infmrgelb  10548  infmrlb  10549  xrinfmss2  11531  algcvgblem  14206  isprm2  14225  oduglb  15769  odulub  15771  isirred2  17350  isdomn2  17948  ntreq0  19578  ist0-3  19846  ist1-3  19850  ordthaus  19885  dfcon2  19920  iscusp2  20805  mdsymlem8  27329  mo5f  27383  iuninc  27428  suppss2f  27477  tosglblem  27657  esumpfinvalf  28082  axrepprim  29074  axacprim  29079  dffr5  29182  dfso2  29183  dfpo2  29184  elpotr  29213  itg2addnclem2  30067  gtinf  30137  isdmn3  30471  sbcimi  30512  moxfr  30624  isdomn3  31164  conss34  31351  onfrALTlem5  33314  onfrALTlem5VD  33685  bnj110  33916  bnj92  33920  bnj539  33949  bnj540  33950  bj-ifim123g  37706  snhesn  37809  psshepw  37811  frege70  37961

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