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  2919  elimhyp  3613  elimhyp2v  3614  elimhyp3v  3615  elimhyp4v  3616  elpwi  3633  elpr2  3659  elpri  3660  elsni  3664  eltpi  3677  snssi  3759  prssi  3771  eloni  4402  limuni2  4453  elxpi  4705  releldmb  4913  relelrnb  4914  funeu  5278  fneu  5348  fvelima  5574  eloprabi  6186  tfrlem9  6401  oeeulem  6599  elqsi  6713  qsel  6738  ecopovsym  6760  elpmi  6789  elmapi  6792  pmsspw  6802  brdomi  6873  undom  6950  mapdom1  7026  ominf  7075  unblem2  7110  unfilem1  7121  fiin  7175  brwdomi  7282  canthwdom  7293  brwdom3i  7297  unxpwdom  7303  scott0  7556  acni  7672  pwcdadom  7842  fin1ai  7919  fin2i  7921  fin4i  7924  ssfin3ds  7956  fin23lem17  7964  fin23lem38  7975  fin23lem39  7976  isfin32i  7991  fin34  8016  isfin7-2  8022  fin1a2lem13  8038  fin12  8039  gchi  8246  wuntr  8327  wununi  8328  wunpw  8329  wunpr  8331  wun0  8340  tskpwss  8374  tskpw  8375  tsken  8376  grutr  8415  grupw  8417  grupr  8419  gruurn  8420  intgru  8436  ingru  8437  grutsk  8444  indpi  8531  eliooord  10710  fzrev3i  10850  elfzole1  10882  elfzolt2  10883  bcm1k  11327  bcp1nk  11329  rere  11607  nn0abscl  11797  climcl  11973  rlimcl  11977  rlimdm  12025  o1res  12034  rlimdmo1  12091  climcau  12144  caucvgb  12152  restsspw  13336  mreiincl  13498  catidex  13576  catcocl  13587  catass  13588  homa1  13869  homahom2  13870  odulat  14249  dlatjmdi  14300  psrel  14312  psref2  14313  pstr2  14314  reldir  14355  dirdm  14356  dirref  14357  dirtr  14358  dirge  14359  submss  14427  subm0cl  14429  submcl  14430  submmnd  14431  subgsubm  14639  symgcl  14778  symginv  14782  odmulg  14869  efgsp1  15046  efgsres  15047  frgpnabl  15163  dprdgrp  15240  dprdf  15241  abvfge0  15587  abveq0  15591  abvmul  15594  abvtri  15595  lbsss  15830  lbssp  15832  lbsind  15833  opsrtoslem2  16226  opsrso  16228  domnchr  16486  cssi  16584  uniopn  16643  iunopn  16644  inopn  16645  fiinopn  16647  eltpsg  16683  basis1  16688  basis2  16689  eltg4i  16698  lmff  17029  t1sep2  17097  cmpfii  17136  kqhmph  17510  fbasne0  17525  0nelfb  17526  fbsspw  17527  fbasssin  17531  ufli  17609  uffixfr  17618  elfm  17642  fclsopni  17710  fclselbas  17711  metflem  17893  xmetf  17894  xmeteq0  17903  xmettri2  17905  tmsxms  18032  tmsms  18033  tngnrg  18185  cncff  18397  cncfi  18398  cfili  18694  iscmet3lem2  18718  mbfres  18999  mbfimaopnlem  19010  limcresi  19235  dvcnp2  19269  ulmcl  19760  ulmf  19761  ulmcau  19772  pserulm  19798  pserdvlem2  19804  sinq34lt0t  19877  logtayl  20007  dchrmhm  20480  lgsdir2lem2  20563  2sqlem9  20612  mulog2sum  20686  tncp  20845  grpofo  20866  grpolidinv  20868  grpoass  20870  opidon  20989  isexid2  20992  nvvop  21165  phpar  21402  pjch1  22249  adjval  22470  ballotlemfp1  23050  bisimp  23121  issgon  23484  pwsiga  23491  measfrge0  23533  measvnul  23536  measvun  23537  umgraf2  23869  elpredim  24176  orderseqlem  24252  eleei  24525  hfun  24808  hfsn  24809  hfelhf  24811  hfuni  24814  hfpw  24815  eloi  25086  preorel  25225  preoref12  25228  preotr1  25234  dupre1  25243  mgmlion  25337  basexre  25522  fneuni  26276  ptfinfin  26298  heibor1lem  26533  heiborlem1  26535  heiborlem3  26537  linds1  27280  linds2  27281  lindsind  27287  lnrfg  27323  symgsssg  27408  symgfisg  27409  symggen  27411  symggen2  27412  psgnunilem5  27417  psgneu  27429  psgnghm2  27438  stoweidlem35  27784  afvelrnb0  28026  afvelima  28029  uslgraf  28104  usgraf  28105  usgraf0  28107  frisusgrapr  28172  trintALTVD  28656  trintALT  28657  bnj916  28965  bnj983  28983  elpcliN  30082
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