MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  ibi Structured version   Visualization version   GIF version

Theorem ibi 256
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
StepHypRef Expression
1 ibi.1 . . 3 (𝜑 → (𝜑𝜓))
21biimpd 219 . 2 (𝜑 → (𝜑𝜓))
32pm2.43i 52 1 (𝜑𝜓)
Colors of variables: wff setvar class
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:  ibir  257  elimh  1029  elimhOLD  1032  elab3gf  3350  elimhyp  4137  elimhyp2v  4138  elimhyp3v  4139  elimhyp4v  4140  elpwi  4159  elsni  4185  elpri  4188  eltpi  4220  snssi  4330  prssi  4344  prelpwi  4906  elxpi  5120  releldmb  5349  relelrnb  5350  elpredim  5680  eloni  5721  limuni2  5774  funeu  5901  fneu  5983  fvelima  6235  eloprabi  7217  fo2ndf  7269  tfrlem9  7466  oeeulem  7666  elqsi  7785  qsel  7811  ecopovsym  7834  elpmi  7861  elmapi  7864  pmsspw  7877  brdomi  7951  undom  8033  mapdom1  8110  ominf  8157  unblem2  8198  unfilem1  8209  fiin  8313  brwdomi  8458  canthwdom  8469  brwdom3i  8473  unxpwdom  8479  scott0  8734  acni  8853  pwcdadom  9023  fin1ai  9100  fin2i  9102  fin4i  9105  ssfin3ds  9137  fin23lem17  9145  fin23lem38  9156  fin23lem39  9157  isfin32i  9172  fin34  9197  isfin7-2  9203  fin1a2lem13  9219  fin12  9220  gchi  9431  wuntr  9512  wununi  9513  wunpw  9514  wunpr  9516  wun0  9525  tskpwss  9559  tskpw  9560  tsken  9561  grutr  9600  grupw  9602  grupr  9604  gruurn  9605  ingru  9622  indpi  9714  eliooord  12218  fzrev3i  12392  elfzole1  12462  elfzolt2  12463  fz1fzo0m1  12499  bcp1nk  13087  rere  13843  nn0abscl  14033  climcl  14211  rlimcl  14215  rlimdm  14263  o1res  14272  rlimdmo1  14329  climcau  14382  caucvgb  14391  fprodcnv  14694  cshws0  15789  restsspw  16073  mreiincl  16237  catidex  16316  catcocl  16327  catass  16328  homa1  16668  homahom2  16669  odulat  17126  dlatjmdi  17178  psrel  17184  psref2  17185  pstr2  17186  reldir  17214  dirdm  17215  dirref  17216  dirtr  17217  dirge  17218  mgmcl  17226  submss  17331  subm0cl  17333  submcl  17334  submmnd  17335  subgsubm  17597  symgbasf1o  17784  symginv  17803  psgneu  17907  odmulg  17954  efgsp1  18131  efgsres  18132  frgpnabl  18259  dprdgrp  18385  dprdf  18386  abvfge0  18803  abveq0  18807  abvmul  18810  abvtri  18811  lbsss  19058  lbssp  19060  lbsind  19061  opsrtoslem2  19466  opsrso  19468  domnchr  19861  cssi  20009  linds1  20130  linds2  20131  lindsind  20137  mdetunilem9  20407  uniopn  20683  iunopn  20684  inopn  20685  fiinopn  20687  eltpsg  20728  basis1  20735  basis2  20736  eltg4i  20745  lmff  21086  t1sep2  21154  cmpfii  21193  ptfinfin  21303  kqhmph  21603  fbasne0  21615  0nelfb  21616  fbsspw  21617  fbasssin  21621  ufli  21699  uffixfr  21708  elfm  21732  fclsopni  21800  fclselbas  21801  ustssxp  21989  ustbasel  21991  ustincl  21992  ustdiag  21993  ustinvel  21994  ustexhalf  21995  ustfilxp  21997  ustbas2  22010  ustbas  22012  psmetf  22092  psmet0  22094  psmettri2  22095  metflem  22114  xmetf  22115  xmeteq0  22124  xmettri2  22126  tmsxms  22272  tmsms  22273  metustsym  22341  tngnrg  22459  cncff  22677  cncfi  22678  cfili  23047  iscmet3lem2  23071  mbfres  23392  mbfimaopnlem  23403  limcresi  23630  dvcnp2  23664  ulmcl  24116  ulmf  24117  ulmcau  24130  pserulm  24157  pserdvlem2  24163  sinq34lt0t  24242  logtayl  24387  dchrmhm  24947  lgsdir2lem2  25032  2sqlem9  25133  mulog2sum  25207  eleei  25758  uhgrf  25938  ushgrf  25939  upgrf  25962  umgrf  25974  uspgrf  26030  usgrf  26031  usgrfs  26033  nbcplgr  26311  clwlkcompim  26657  tncp  27300  eulplig  27307  grpofo  27323  grpolidinv  27325  grpoass  27327  nvvop  27434  phpar  27649  pjch1  28499  toslub  29642  tosglb  29644  orngsqr  29778  zhmnrg  29985  issgon  30160  measfrge0  30240  measvnul  30243  measvun  30246  fzssfzo  30587  bnj916  30977  bnj983  30995  mfsdisj  31421  mtyf2  31422  maxsta  31425  mvtinf  31426  orderseqlem  31723  hfun  32260  hfsn  32261  hfelhf  32263  hfuni  32266  hfpw  32267  fneuni  32317  bj-elid  33056  mptsnunlem  33156  heibor1lem  33579  heiborlem1  33581  heiborlem3  33583  opidonOLD  33622  isexid2  33625  elpcliN  34998  lnrfg  37508  pwinfi2  37686  frege55lem1c  38030  gneispacef  38253  gneispacef2  38254  gneispacern2  38257  gneispace0nelrn  38258  gneispaceel  38261  gneispacess  38263  trintALTVD  38936  trintALT  38937  eliuniin  39099  eliuniin2  39123  disjrnmpt2  39191  fvelimad  39274  stoweidlem35  40015  saluncl  40300  saldifcl  40302  0sal  40303  sge0resplit  40386  omedm  40476  afvelrnb0  41007  afvelima  41010  rlimdmafv  41020  submgmss  41557  submgmcl  41559  submgmmgm  41560  asslawass  41594  linindsi  42001
  Copyright terms: Public domain W3C validator