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

Theorem ibi 232
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 198 . 2  |-  ( ph  ->  ( ph  ->  ps ) )
32pm2.43i 43 1  |-  ( ph  ->  ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 176
This theorem is referenced by:  ibir  233  elimh  922  elab3gf  2932  elimhyp  3626  elimhyp2v  3627  elimhyp3v  3628  elimhyp4v  3629  elpwi  3646  elpr2  3672  elpri  3673  elsni  3677  eltpi  3690  snssi  3775  prssi  3787  eloni  4418  limuni2  4469  elxpi  4721  releldmb  4929  relelrnb  4930  funeu  5294  fneu  5364  fvelima  5590  eloprabi  6202  tfrlem9  6417  oeeulem  6615  elqsi  6729  qsel  6754  ecopovsym  6776  elpmi  6805  elmapi  6808  pmsspw  6818  brdomi  6889  undom  6966  mapdom1  7042  ominf  7091  unblem2  7126  unfilem1  7137  fiin  7191  brwdomi  7298  canthwdom  7309  brwdom3i  7313  unxpwdom  7319  scott0  7572  acni  7688  pwcdadom  7858  fin1ai  7935  fin2i  7937  fin4i  7940  ssfin3ds  7972  fin23lem17  7980  fin23lem38  7991  fin23lem39  7992  isfin32i  8007  fin34  8032  isfin7-2  8038  fin1a2lem13  8054  fin12  8055  gchi  8262  wuntr  8343  wununi  8344  wunpw  8345  wunpr  8347  wun0  8356  tskpwss  8390  tskpw  8391  tsken  8392  grutr  8431  grupw  8433  grupr  8435  gruurn  8436  intgru  8452  ingru  8453  grutsk  8460  indpi  8547  eliooord  10726  fzrev3i  10866  elfzole1  10898  elfzolt2  10899  bcm1k  11343  bcp1nk  11345  rere  11623  nn0abscl  11813  climcl  11989  rlimcl  11993  rlimdm  12041  o1res  12050  rlimdmo1  12107  climcau  12160  caucvgb  12168  restsspw  13352  mreiincl  13514  catidex  13592  catcocl  13603  catass  13604  homa1  13885  homahom2  13886  odulat  14265  dlatjmdi  14316  psrel  14328  psref2  14329  pstr2  14330  reldir  14371  dirdm  14372  dirref  14373  dirtr  14374  dirge  14375  submss  14443  subm0cl  14445  submcl  14446  submmnd  14447  subgsubm  14655  symgcl  14794  symginv  14798  odmulg  14885  efgsp1  15062  efgsres  15063  frgpnabl  15179  dprdgrp  15256  dprdf  15257  abvfge0  15603  abveq0  15607  abvmul  15610  abvtri  15611  lbsss  15846  lbssp  15848  lbsind  15849  opsrtoslem2  16242  opsrso  16244  domnchr  16502  cssi  16600  uniopn  16659  iunopn  16660  inopn  16661  fiinopn  16663  eltpsg  16699  basis1  16704  basis2  16705  eltg4i  16714  lmff  17045  t1sep2  17113  cmpfii  17152  kqhmph  17526  fbasne0  17541  0nelfb  17542  fbsspw  17543  fbasssin  17547  ufli  17625  uffixfr  17634  elfm  17658  fclsopni  17726  fclselbas  17727  metflem  17909  xmetf  17910  xmeteq0  17919  xmettri2  17921  tmsxms  18048  tmsms  18049  tngnrg  18201  cncff  18413  cncfi  18414  cfili  18710  iscmet3lem2  18734  mbfres  19015  mbfimaopnlem  19026  limcresi  19251  dvcnp2  19285  ulmcl  19776  ulmf  19777  ulmcau  19788  pserulm  19814  pserdvlem2  19820  sinq34lt0t  19893  logtayl  20023  dchrmhm  20496  lgsdir2lem2  20579  2sqlem9  20628  mulog2sum  20702  tncp  20861  grpofo  20882  grpolidinv  20884  grpoass  20886  opidon  21005  isexid2  21008  nvvop  21181  phpar  21418  pjch1  22265  adjval  22486  ballotlemfp1  23066  bisimp  23137  issgon  23499  pwsiga  23506  measfrge0  23548  measvnul  23551  measvun  23552  umgraf2  23884  elpredim  24247  orderseqlem  24323  eleei  24597  hfun  24880  hfsn  24881  hfelhf  24883  hfuni  24886  hfpw  24887  eloi  25189  preorel  25328  preoref12  25331  preotr1  25337  dupre1  25346  mgmlion  25440  basexre  25625  fneuni  26379  ptfinfin  26401  heibor1lem  26636  heiborlem1  26638  heiborlem3  26640  linds1  27383  linds2  27384  lindsind  27390  lnrfg  27426  symgsssg  27511  symgfisg  27512  symggen  27514  symggen2  27515  psgnunilem5  27520  psgneu  27532  psgnghm2  27541  stoweidlem35  27887  afvelrnb0  28132  afvelima  28135  rlimdmafv  28145  uslgraf  28236  usgraf  28237  usgraf0  28239  frisusgrapr  28418  trintALTVD  28972  trintALT  28973  bnj916  29281  bnj983  29299  elpcliN  30704
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 177
  Copyright terms: Public domain W3C validator