Theorem ibi 241

Description: Inference that converts a biconditional implied by one of its arguments, into an implication. (Contributed by NM, 17-Oct-2003.)

Hypothesis

Ref	Expression
ibi.1

Assertion

Ref	Expression
ibi

Proof of Theorem ibi

Step	Hyp	Ref	Expression
1		ibi.1	. . 3
2	1	biimpd 207	. 2
3	2	pm2.43i 47	1

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

This theorem is referenced by:  ibir  242  elimh  956  elab3gf  3251  elimhyp  4000  elimhyp2v  4001  elimhyp3v  4002  elimhyp4v  4003  elpwi  4021  elpr2  4048  elpri  4049  elsni  4054  eltpi  4073  snssi  4174  prssi  4186  eloni  4893  limuni2  4944  elxpi  5020  releldmb  5242  relelrnb  5243  funeu  5617  fneu  5690  fvelima  5925  eloprabi  6862  fo2ndf  6907  tfrlem9  7073  oeeulem  7269  elqsi  7384  qsel  7409  ecopovsym  7432  elpmi  7457  elmapi  7460  pmsspw  7473  brdomi  7547  undom  7625  mapdom1  7702  ominf  7752  unblem2  7793  unfilem1  7804  fiin  7902  brwdomi  8015  canthwdom  8026  brwdom3i  8030  unxpwdom  8036  scott0  8325  acni  8447  pwcdadom  8617  fin1ai  8694  fin2i  8696  fin4i  8699  ssfin3ds  8731  fin23lem17  8739  fin23lem38  8750  fin23lem39  8751  isfin32i  8766  fin34  8791  isfin7-2  8797  fin1a2lem13  8813  fin12  8814  gchi  9023  wuntr  9104  wununi  9105  wunpw  9106  wunpr  9108  wun0  9117  tskpwss  9151  tskpw  9152  tsken  9153  grutr  9192  grupw  9194  grupr  9196  gruurn  9197  ingru  9214  indpi  9306  eliooord  11613  fzrev3i  11775  elfzole1  11836  elfzolt2  11837  bcp1nk  12395  rere  12955  nn0abscl  13145  climcl  13322  rlimcl  13326  rlimdm  13374  o1res  13383  rlimdmo1  13440  climcau  13493  caucvgb  13502  fprodcnv  13787  cshws0  14586  restsspw  14829  mreiincl  14993  catidex  15071  catcocl  15082  catass  15083  homa1  15364  homahom2  15365  odulat  15775  dlatjmdi  15827  psrel  15833  psref2  15834  pstr2  15835  reldir  15863  dirdm  15864  dirref  15865  dirtr  15866  dirge  15867  mgmcl  15875  submss  15981  subm0cl  15983  submcl  15984  submmnd  15985  subgsubm  16223  symgbasf1o  16408  symginv  16427  psgneu  16531  odmulg  16578  efgsp1  16755  efgsres  16756  frgpnabl  16879  dprdgrp  17038  dprdf  17039  abvfge0  17471  abveq0  17475  abvmul  17478  abvtri  17479  lbsss  17723  lbssp  17725  lbsind  17726  opsrtoslem2  18149  opsrso  18151  domnchr  18569  cssi  18715  linds1  18845  linds2  18846  lindsind  18852  mdetunilem9  19122  uniopn  19406  iunopn  19407  inopn  19408  fiinopn  19410  eltpsg  19446  basis1  19451  basis2  19452  eltg4i  19461  lmff  19802  t1sep2  19870  cmpfii  19909  ptfinfin  20020  kqhmph  20320  fbasne0  20331  0nelfb  20332  fbsspw  20333  fbasssin  20337  ufli  20415  uffixfr  20424  elfm  20448  fclsopni  20516  fclselbas  20517  ustssxp  20707  ustbasel  20709  ustincl  20710  ustdiag  20711  ustinvel  20712  ustexhalf  20713  ustfilxp  20715  ustbas2  20728  ustbas  20730  psmetf  20810  psmet0  20812  psmettri2  20813  metflem  20831  xmetf  20832  xmeteq0  20841  xmettri2  20843  tmsxms  20989  tmsms  20990  metustsymOLD  21064  metustsym  21065  tngnrg  21183  cncff  21397  cncfi  21398  cfili  21707  iscmet3lem2  21731  mbfres  22051  mbfimaopnlem  22062  limcresi  22289  dvcnp2  22323  ulmcl  22776  ulmf  22777  ulmcau  22790  pserulm  22817  pserdvlem2  22823  sinq34lt0t  22902  logtayl  23041  dchrmhm  23516  lgsdir2lem2  23599  2sqlem9  23648  mulog2sum  23722  eleei  24200  uhgraf  24299  ushgraf  24302  umgraf2  24317  uslgraf  24345  usgraf  24346  usgraf0  24348  clwwisshclww  24807  frisusgrapr  24991  tncp  25180  grpofo  25201  grpolidinv  25203  grpoass  25205  opidonOLD  25324  isexid2  25327  nvvop  25502  phpar  25739  pjch1  26588  toslub  27656  tosglb  27658  orngsqr  27794  zhmnrg  27948  issgon  28123  measfrge0  28174  measvnul  28177  measvun  28180  fzssfzo  28490  mfsdisj  28910  mtyf2  28911  maxsta  28914  mvtinf  28915  elpredim  29256  orderseqlem  29332  hfun  29835  hfsn  29836  hfelhf  29838  hfuni  29841  hfpw  29842  fneuni  30165  heibor1lem  30305  heiborlem1  30307  heiborlem3  30309  lnrfg  31068  stoweidlem35  31817  afvelrnb0  32249  afvelima  32252  rlimdmafv  32262  uhgf  32368  submgmss  32480  submgmcl  32482  submgmmgm  32483  asslawass  32517  linindsi  33048  trintALTVD  33680  trintALT  33681  bnj916  33991  bnj983  34009  bj-elimhyp  34160  bj-elid  34599  elpcliN  35617  pwinfi2  37747  frege55lem1c  37943

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