Theorem mpbir 190

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

Hypotheses

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

Assertion

Ref	Expression
mpbir	|- ph

Proof of Theorem mpbir

Step	Hyp	Ref	Expression
1		mpbir.min	. 2 |- ps
2		mpbir.maj	. . 3 |- (ph <-> ps)
3	2	biimpr 152	. 2 |- (ps -> ph)
4	1, 3	ax-mp 7	1 |- ph

Syntax hints:   <-> wb 146

This theorem is referenced by:  mtbir 192  orri 231  imp 350  con4bii 521  pm3.2ni 578  pm5.74ri 585  pm3.24 655  pm5.16 664  mpbir2an 727  nicodmpraw 949  19.35ri 1053  ax9 1110  a9e 1112  cbval2 1298  cbvex2 1299  moaneu 1407  moanmo 1408  axext 1437  eqeltr 1520  mprgbir 1677  visset 1788  issetri 1791  eueq3 1891  moeq 1892  ru 1909  eqsstr 2062  3sstr4 2071  ssnpss 2120  pwid 2379  pri1 2420  pwv 2470  uni0 2493  intab 2528  eqbrtr 2602  tr0 2659  trv 2660  zfrep4 2669  zfnuleu 2675  0ex 2679  inex1 2684  0elpw 2704  notzfaus 2709  pwex 2713  snex 2718  exss 2737  dvdemo1 2743  zfpair2 2748  moop2 2766  itlso 2827  uniex2 2833  rabxfr 2865  0elon 2985  nsuceq0 3016  limon 3057  onuninsuc 3071  finds 3119  finds2 3121  tfinds2 3128  onxpdisj 3203  relsn 3216  relxp 3217  relopab 3228  rel0 3234  reli 3235  rele 3236  dmi 3283  relres 3338  relcnv 3386  relco 3430  cnvcnv 3432  isarep2 3518  opabex 3549  f0 3595  fconst 3597  f10 3652  f1o00 3653  f1oi 3656  f1osn 3658  fvopab3ig 3717  fvi 3781  canth 3846  ncanth 3847  tfrlem8 3857  tz7.44lem1 3866  abianfp 3901  reloprab 3931  reldmoprab 3944  oprabex 3958  oprabex3 3961  oprabvalig 3963  oprabval3 3969  ndmoprcl 3984  fo1st 4029  fo2nd 4030  f1stres 4031  f2ndres 4032  df1st2 4064  df2nd2 4065  1ne0 4080  0lt1o 4085  th3qcor 4254  mapsspw 4279  map0 4282  relen 4308  reldom 4309  ssdomg 4343  ensn1 4359  limensuci 4438  omsdomnn 4461  unblem4 4472  prfi 4483  pm54.43 4498  inf2 4532  inf3lem6 4542  infeq5 4545  zfinf 4550  inf5 4552  trcl 4569  r1fnon 4574  r1tr 4578  tz9.12lem2 4584  tz9.12lem3 4585  jech9.3 4590  rankval 4592  rankr1 4598  rankpw 4608  karden 4650  aceq3lem 4656  ac2 4670  kmlem2 4690  numthlem 4707  numth2 4709  zorn 4721  cardon 4751  cardid 4752  sucxpdom 4769  ondomon 4779  cardprc 4784  alephfnon 4785  alephsucpw 4793  alephsucdom 4803  alephfplem4 4822  alephfp 4823  alephval3 4826  axpowndlem3 4874  zfcndun 4890  zfcndpow 4891  zfcndinf 4893  zfcndac 4894  dmaddpi 4941  dmmulpi 4942  1lt2pi 4955  1q 4980  1lt2pq 5001  1pr 5040  0r 5112  1r 5113  m1r 5114  m1p1sr 5124  m1m1sr 5125  0lt1sr 5127  axaddopr 5188  axmulopr 5189  ax1cn 5192  ax1ne0 5203  subaddri 5295  ine0 5357  pnfxr 5416  mnfxr 5417  pnfnre 5419  mnfnre 5420  pnfnemnf 5460  renfdisj 5463  mnfltpnf 5468  divrec 5651  div1 5679  recgt0i 5721  nn1suc 5838  4d2e2 5925  nnunb 5968  arch 5969  0z 6044  nneo 6095  om2uzran 6188  om2uzf1o 6189  uzrdgfnuz 6194  ndmioo 6258  ioof 6284  indstr 6344  elfzlem 6356  seq0fn 6429  dfseq0 6446  sq0 6517  sqrlem6 6559  sqrlem8 6561  sqrlem11 6564  sqr4 6598  sqr9 6599  sqr2irr 6610  irec 6612  nthruz 6628  cjmulrcl 6677  abs0 6765  abstri 6780  abslem2i 6796  bcpasc2 6856  climrel 6865  climuz0 6996  iserzshft 7031  climabslem 7035  climubi 7040  climsup 7042  caucvg 7050  isumshft2 7091  isumcmpi 7101  infcvgaux1 7105  fnsmnt 7112  negfcncf 7155  ivthlem5 7171  ivthlem6 7172  ivthlem7 7173  ivthlem8 7174  isupivth 7176  ivthlem5OLD 7180  ivthlem6OLD 7181  ivthlem7OLD 7182  ivthlem8OLD 7183  ivth2OLD 7185  efaddlem8 7238  efaddlem12 7242  ef1tllem 7274  eirrlem1 7281  eirrlem3 7283  eirr 7286  reeff1o 7319  sinadd 7344  cos2tOLD 7357  cos1bnd 7367  cos2bnd 7368  acdc2lem2 7382  acdc5lem2 7385  nnenom 7391  unbenlem 7398  ruclem13 7416  ruclem35 7438  aleph1re 7445  eltopsp 7497  tpsex 7498  subbas 7537  sn0top 7540  indistps 7546  distps 7547  retopbas 7548  msrel 7684  0met 7713  cnmet 7791  bcthlem12 7892  isgrpi 7924  0ngrp 7937  isgrp2i 7959  issubgi 8007  grpsn 8009  ablsn 8010  ghgrpilem4 8021  ghsubgi 8023  isring 8026  vcrel 8051  isvci 8053  nvrel 8101  0vfval 8105  isnvi 8110  vsfval 8132  ipcl 8234  ajmoi 8385  ajfuni 8386  minvecdist 8451  pilem2 8504  sincosq1lem 8533  sincos4thpi 8540  sincos6thpi 8541  cosh111lem1 8542  efifolem2 8551  circgrpOLD 8571  logrn 8586  eff1o2 8589  logf1o 8590  relogf1o 8592  log1 8601  loge 8602  pilog 8603  relogiso 8610  log1OLD 8620  logeOLD 8621  logisoOLD 8627  axgroth2 8630  axgroth3 8631  ghomgrpilem2 8653  symggrpi 8673  symgidi 8674  ompfl2 8687  cmpfun 8722  hmeogrp 8776  efilcp 8795  efilcp2 8800  dtopcl 8809  1ded 8865  relded 8867  reldded 8868  relrded 8869  relcat 8888  reldcat 8889  relrcat 8890  hgrarel 8950  avril1 8964  2bornot2b 8965  normlem2 9126  norm3adif 9164  projlem13 9328  projlem14 9329  pjpj0 9384  shscl 9410  shsumval2 9489  h1de2 9605  fh3 9697  fh4 9698  qlaxr3 9708  ho0f 9808  hoif 9811  hodid 9844  ho0sub 9852  hosd1 9879  adjmo 9889  nmopsetn0 9923  nmfnsetn0 9936  funadj 9944  funcnvadj 9948  adj1o 9949  nlelsh 10122  cnlnadjlem8 10136  nmoptri2 10160  bra11 10168  pjoc 10232  pjinvar 10243  cvnsymt 10341

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

This theorem depends on definitions:  df-bi 147

Copyright terms: Public domain