Theorem impbid1 215

Description: Infer an equivalence from two implications. (Contributed by NM, 6-Mar-2007.)

Hypotheses

Ref	Expression
impbid1.1	|- ( ph -> ( ps -> ch ) )
impbid1.2	|- ( ch -> ps )

Assertion

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

Proof of Theorem impbid1

Step	Hyp	Ref	Expression
1		impbid1.1	. 2 |- ( ph -> ( ps -> ch ) )
2		impbid1.2	. . 3 |- ( ch -> ps )
3	2	a1i 11	. 2 |- ( ph -> ( ch -> ps ) )
4	1, 3	impbid 202	1 |- ( ph -> ( ps <-> ch ) )

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

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 197

This theorem is referenced by:  impbid2  216  iba  524  ibar  525  pm5.71  977  cad0  1556  19.33b  1813  19.40b  1815  19.9t  2071  axc16gb  2136  19.9tOLD  2204  equs5  2351  sb4b  2358  2eu1  2553  2eu3  2555  ceqsalgALT  3231  eqvincg  3329  csbprcOLD  3981  undif4  4035  ssprsseq  4357  sneqbg  4374  preq1b  4377  opthpr  4384  elpwuni  4616  disjxiun  4649  eusv2i  4863  reusv2lem3  4871  reusv3  4876  reuxfr2d  4891  soltmin  5532  ssxpb  5568  xp11  5569  xpcan  5570  xpcan2  5571  ordssun  5827  suc11  5831  unizlim  5844  imadif  5973  2elresin  6002  mpteqb  6299  f1fveq  6519  f1elima  6520  f1imass  6521  fliftf  6565  sorpssuni  6946  sorpssint  6947  iunpw  6978  ssonprc  6992  onint0  6996  oa00  7639  omcan  7649  omopth2  7664  oecan  7669  nnarcl  7696  iserd  7768  ecopoverOLD  7852  map0g  7897  fundmen  8030  fopwdom  8068  onfin  8151  fineqvlem  8174  f1finf1o  8187  isfiniteg  8220  inficl  8331  tc00  8624  cardnueq0  8790  cardsdomel  8800  wdomfil  8884  wdomnumr  8887  alephsucdom  8902  cardalephex  8913  dfac12lem2  8966  cfeq0  9078  fin23lem24  9144  fin1a2lem9  9230  carden  9373  axrepnd  9416  axacndlem4  9432  gchpwdom  9492  gchina  9521  r1tskina  9604  addcanpi  9721  mulcanpi  9722  elnpi  9810  addcan  10220  addcan2  10221  neg11  10332  negreb  10346  add20  10540  mulcand  10660  cru  11012  nn0lt10b  11439  uz11  11710  eqreznegel  11774  lbzbi  11776  rpnnen1lem6  11819  rpnnen1OLD  11825  xrmaxlt  12012  xrltmin  12013  xrmaxle  12014  xrlemin  12015  xneg11  12046  xnn0xadd0  12077  xsubge0  12091  xrub  12142  elioc2  12236  elico2  12237  elicc2  12238  fzopth  12378  2ffzeq  12460  flidz  12611  addmodlteq  12745  expeq0  12890  sq01  12986  fz1eqb  13145  hashen1  13160  hash1snb  13207  hashle2pr  13259  wrdnval  13335  eqwrd  13346  ccatalpha  13375  wrdl1s1  13394  ccatopth  13470  ccatopth2  13471  wrdlen2  13688  cj11  13902  sqrt0  13982  abs00  14029  recan  14076  rlimdm  14282  rpnnen2lem12  14954  0dvds  15002  dvds1  15041  alzdvds  15042  nn0enne  15094  nn0oddm1d2  15101  nnoddm1d2  15102  gcdeq0  15238  algcvgblem  15290  prmexpb  15430  prmreclem3  15622  4sqlem11  15659  moni  16396  grprcan  17455  grplcan  17477  grpinv11  17484  galcan  17737  sylow2a  18034  subgdisjb  18106  drngmuleq0  18770  lspsncmp  19116  fidomndrng  19307  coe1tm  19643  xrsdsreclb  19793  znidomb  19910  lmisfree  20181  tgdom  20782  en1top  20788  cmpfi  21211  txcmpb  21447  hmeocnvb  21577  flimcls  21789  hauspwpwf1  21791  flftg  21800  ghmcnp  21918  metrest  22329  icoopnst  22738  iocopnst  22739  ishl2  23166  vitali  23382  mbfi1fseqlem4  23485  aannenlem1  24083  perfect  24956  2lgsoddprmlem3  25139  umgrislfupgrlem  26017  usgrausgrb  26064  cplgruvtxb  26311  upgriswlk  26537  uhgrwkspth  26651  usgr2wlkspth  26655  usgr2trlspth  26657  usgr2pthspth  26658  extwwlkfab  27223  grporcan  27372  grpolcan  27384  ip2eqi  27712  hial2eq  27963  eigorthi  28696  stge1i  29097  stle0i  29098  mdbr3  29156  mdbr4  29157  atsseq  29206  mdsymlem7  29268  reuxfr3d  29329  disjunsn  29407  fpwrelmapffslem  29507  xmulcand  29629  prsdm  29960  prsrn  29961  mthmpps  31479  untangtr  31591  funeldmb  31661  sltval2  31809  filnetlem4  32376  ordtopconn  32438  ordtopt0  32441  bj-dfbi6  32560  bj-19.9htbi  32694  icorempt2  33199  wl-lem-moexsb  33350  seqpo  33543  lshpcmp  34275  lsatcmp  34290  lsatcmp2  34291  ltrneq2  35434  ltrneq  35435  tendospcanN  36312  dochlkr  36674  lcfl7N  36790  hgmap11  37194  fphpd  37380  pellexlem3  37395  qirropth  37473  expdioph  37590  rpnnen3  37599  iotasbc  38620  2reu1  41186  2reu3  41188  rlimdmafv  41257  funop1  41302  fzoopth  41337  2ffzoeq  41338  evenprm2  41623  perfectALTV  41632  nnsum3primesle9  41682  upgrwlkupwlkb  41722  0ringdif  41870  islinindfis  42238  lincresunit3lem3  42263  blen1b  42382