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

Theorem ibi 249
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  |-  ( ph  ->  ( ph  <->  ps )
)
Assertion
Ref Expression
ibi  |-  ( ph  ->  ps )

Proof of Theorem ibi
StepHypRef Expression
1 ibi.1 . . 3  |-  ( ph  ->  ( ph  <->  ps )
)
21biimpd 212 . 2  |-  ( ph  ->  ( ph  ->  ps ) )
32pm2.43i 49 1  |-  ( ph  ->  ps )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 189
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 190
This theorem is referenced by:  ibir  250  elimh  973  elab3gf  3201  elimhyp  3950  elimhyp2v  3951  elimhyp3v  3952  elimhyp4v  3953  elpwi  3971  elpri  3996  elsni  4004  eltpi  4027  snssi  4128  prssi  4140  elxpi  4868  releldmb  5087  relelrnb  5088  elpredim  5410  eloni  5451  limuni2  5502  funeu  5624  fneu  5701  fvelima  5939  eloprabi  6881  fo2ndf  6929  tfrlem9  7128  oeeulem  7327  elqsi  7442  qsel  7467  ecopovsym  7490  elpmi  7515  elmapi  7518  pmsspw  7531  brdomi  7605  undom  7685  mapdom1  7762  ominf  7809  unblem2  7849  unfilem1  7860  fiin  7961  brwdomi  8108  canthwdom  8119  brwdom3i  8123  unxpwdom  8129  scott0  8382  acni  8501  pwcdadom  8671  fin1ai  8748  fin2i  8750  fin4i  8753  ssfin3ds  8785  fin23lem17  8793  fin23lem38  8804  fin23lem39  8805  isfin32i  8820  fin34  8845  isfin7-2  8851  fin1a2lem13  8867  fin12  8868  gchi  9074  wuntr  9155  wununi  9156  wunpw  9157  wunpr  9159  wun0  9168  tskpwss  9202  tskpw  9203  tsken  9204  grutr  9243  grupw  9245  grupr  9247  gruurn  9248  ingru  9265  indpi  9357  eliooord  11722  fzrev3i  11890  elfzole1  11958  elfzolt2  11959  fz1fzo0m1  11993  bcp1nk  12533  rere  13233  nn0abscl  13423  climcl  13611  rlimcl  13615  rlimdm  13663  o1res  13672  rlimdmo1  13729  climcau  13782  caucvgb  13794  fprodcnv  14085  cshws0  15120  restsspw  15378  mreiincl  15550  catidex  15628  catcocl  15639  catass  15640  homa1  15980  homahom2  15981  odulat  16439  dlatjmdi  16491  psrel  16497  psref2  16498  pstr2  16499  reldir  16527  dirdm  16528  dirref  16529  dirtr  16530  dirge  16531  mgmcl  16539  submss  16645  subm0cl  16647  submcl  16648  submmnd  16649  subgsubm  16887  symgbasf1o  17072  symginv  17091  psgneu  17195  odmulg  17255  efgsp1  17435  efgsres  17436  frgpnabl  17559  dprdgrp  17685  dprdf  17686  abvfge0  18098  abveq0  18102  abvmul  18105  abvtri  18106  lbsss  18348  lbssp  18350  lbsind  18351  opsrtoslem2  18756  opsrso  18758  domnchr  19151  cssi  19295  linds1  19416  linds2  19417  lindsind  19423  mdetunilem9  19693  uniopn  19975  iunopn  19976  inopn  19977  fiinopn  19979  eltpsg  20008  basis1  20013  basis2  20014  eltg4i  20023  lmff  20365  t1sep2  20433  cmpfii  20472  ptfinfin  20582  kqhmph  20882  fbasne0  20893  0nelfb  20894  fbsspw  20895  fbasssin  20899  ufli  20977  uffixfr  20986  elfm  21010  fclsopni  21078  fclselbas  21079  ustssxp  21267  ustbasel  21269  ustincl  21270  ustdiag  21271  ustinvel  21272  ustexhalf  21273  ustfilxp  21275  ustbas2  21288  ustbas  21290  psmetf  21370  psmet0  21372  psmettri2  21373  metflem  21391  xmetf  21392  xmeteq0  21401  xmettri2  21403  tmsxms  21549  tmsms  21550  metustsym  21618  tngnrg  21725  cncff  21973  cncfi  21974  cfili  22286  iscmet3lem2  22310  mbfres  22648  mbfimaopnlem  22659  limcresi  22888  dvcnp2  22922  ulmcl  23384  ulmf  23385  ulmcau  23398  pserulm  23425  pserdvlem2  23431  sinq34lt0t  23512  logtayl  23653  dchrmhm  24217  lgsdir2lem2  24300  2sqlem9  24349  mulog2sum  24423  eleei  24975  uhgraf  25074  ushgraf  25077  umgraf2  25092  uslgraf  25120  usgraf  25121  usgraf0  25123  clwwisshclww  25583  frisusgrapr  25767  tncp  25958  grpofo  25975  grpolidinv  25977  grpoass  25979  opidonOLD  26098  isexid2  26101  nvvop  26276  phpar  26513  pjch1  27371  toslub  28477  tosglb  28479  tosglbOLD  28480  orngsqr  28615  zhmnrg  28819  issgon  28993  measfrge0  29073  measvnul  29076  measvun  29079  fzssfzo  29470  bnj916  29792  bnj983  29810  mfsdisj  30236  mtyf2  30237  maxsta  30240  mvtinf  30241  orderseqlem  30538  hfun  30993  hfsn  30994  hfelhf  30996  hfuni  30999  hfpw  31000  fneuni  31051  bj-elimhyp  31197  bj-elid  31684  mptsnunlem  31784  heibor1lem  32185  heiborlem1  32187  heiborlem3  32189  elpcliN  33502  lnrfg  36022  pwinfi2  36210  frege55lem1c  36556  trintALTVD  37316  trintALT  37317  disjrnmpt2  37500  stoweidlem35  37933  saluncl  38215  saldifcl  38217  sge0resplit  38285  afvelrnb0  38703  afvelima  38706  rlimdmafv  38716  uhgrf  39198  ushgrf  39199  upgrf  39224  umgrf  39234  uspgrf  39288  usgrf  39289  usgrfs  39291  clWlkcompim  39805  uhgfALTV  39952  submgmss  40064  submgmcl  40066  submgmmgm  40067  asslawass  40101  linindsi  40512
  Copyright terms: Public domain W3C validator