Theorem mpbi 164

Description: An inference from a biconditional, related to modus ponens.

Hypotheses

Ref	Expression
mpbi.min	|- ph
mpbi.maj	|- (ph <-> ps)

Assertion

Ref	Expression
mpbi	|- ps

Proof of Theorem mpbi

Step	Hyp	Ref	Expression
1		mpbi.min	. 2 |- ph
2		mpbi.maj	. . 3 |- (ph <-> ps)
3	2	biimp 133	. 2 |- (ph -> ps)
4	1, 3	ax-mp 6	1 |- ps

Syntax hints:   <-> wb 127

This theorem is referenced by:  mtbi 166  ori 200  pm5.74i 443  pm4.71i 483  pm4.71ri 484  pm5.32i 489  biluk 512  19.35i 755  19.36i 758  exan 784  sbco 910  19.37aiv 962  axun 1081  axpow 1082  axinf 1084  axac 1085  cleqcomi 1105  eqtr 1119  eleqtr 1161  nrex 1270  isseti 1352  vtocl2 1379  vtocl3 1380  eueq1 1428  euxfr2 1435  ru 1437  zfaus 1480  bm1.3ii 1481  ssid 1519  sseqtr 1532  reuxfr2 1579  unssi 1633  ssini 1660  dfin4 1673  noel 1711  rab0 1718  difid 1755  difdisj 1758  snid 1830  dtru 1889  unop 1931  op1stb 1992  breqtr 2080  fr0 2179  onunisuc 2354  omon 2384  brinxp 2466  dmsnsn0 2544  rn0 2567  dmresi 2600  cnvcnv 2661  co01 2664  fnresi 2737  fnopab 2746  f1cnv 2782  f1ovi 2826  fvi 2900  tfrlem13 2961  tz7.44-2 2967  tz7.44-3 2968  frfnom 2989  f1stres 3096  2o 3110  oawordeulem 3156  ersym 3209  ertr 3211  0nelqs 3234  dfdom2 3288  dmen 3310  ssdomg 3311  pw2en 3348  sbthlem5 3353  mapdom2lem 3388  limensuci 3401  fiint 3445  suc11reg 3456  inf4 3473  tz9.13 3507  rankval 3512  ssrankr1 3520  rankpw 3528  cp 3547  bnd 3548  karden 3551  ac3 3568  ac5 3573  ac6lem 3575  kmlem10 3589  card0 3630  cardom 3632  cardval 3633  cardlim 3657  alephsuc 3672  aleph1 3676  alephgeom 3687  cffnon 3702  cf0 3705  cfsuc 3709  cdaassen 3725  dmaddpi 3812  dmmulpi 3813  1lt2pi 3826  dmrecpq 3868  1lt2pq 3872  subaddeq 4146  renegcl 4171  divval 4217  divcan2 4224  lt01 4377  eqneg 4378  negn0 4380  recgt0i 4385  posex 4422  nnsub 4450  nnunb 4520  ine0 4524  nn0mulcl 4553  nn0ltp1let 4556  nn0ge0i 4559  nn0addge1 4560  nn0ssz 4578  elnnz1 4581  halfnz 4586  zltp1let 4597  indstr 4611  nnlesq 4718  nneo 4719  nnesq 4720  nn0opthlem2 4723  sqrlem1 4731  sqrlem2 4732  sqrlem10 4740  sqrlem11 4741  sqrlem15 4745  sqrlem16 4746  sqrlem19 4749  sqrlem20 4750  sqrmuli 4762  sqr2irrlem1 4777  sqr2irrlem3 4779  nthruc 4784  ipcn 4820  cjmulval 4822  re0 4833  im0 4834  cj0 4835  absgt0 4842  absid 4850  absre 4854  releabs 4858  abstri 4859  abslem2i 4866  facnnt 4870  fac0 4871  climunii 4883  ruclem6 4890  ruclem8 4892  ruclem17 4901  ruclem25 4909  ruclem26 4910  ruclem27 4911  infdif 4948  normlem1 5063  normlem6 5068  normlem7 5069  norm-ii 5086  hlimunii 5143  projlem3 5195  projlem5 5197  projlem12 5204  projlem14 5206  projlem15 5207  projlem18 5210  shincl 5332  shsumval2 5361  chj0 5377  chincl 5382  chdmm1 5398  shjshs 5412  chsup0 5453  spansnpj 5481  cmcmlem 5500  cmcmi 5506  cmcm2i 5507  cmcm3i 5508  fh1 5518  fh2 5519  pjidm 5563  pjssm 5572  pj0 5581  pjocin 5583  pjrn 5587  hosf 5602  hodf 5603  hoscom 5605  hosass 5607  hosdir 5609  hoddir 5610  ho0 5612  hoid0 5614  hoid1 5617  hoid1r 5618  hodseq 5619  pjsdi 5625  pjddi 5626  pjidmco 5642  pjtot 5644  pjin1 5646  pjclem1 5649  stji1 5683  large 5700

This theorem was proved from axioms:  ax-1 3  ax-2 4  ax-3 5  ax-mp 6

This theorem depends on definitions:  df-bi 128

metamath.org