Theorem mpbir 146

Description: An inference from a biconditional, related to modus ponens. (Contributed by NM, 5-Aug-1993.)

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	biimpri 133	. 2 |- ( ps -> ph )
4	1, 3	ax-mp 5	1 |- ph

Syntax hints:   <-> wb 105

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  pm5.74ri  181  imnani  695  stabnot  838  mpbir2an  948  mpbir3an  1203  tru  1399  dcfromnotnotr  1490  dcfromcon  1491  dcfrompeirce  1492  mpgbir  1499  nfxfr  1520  19.8a  1636  sbt  1830  dveeq2  1861  dveeq2or  1862  sbequilem  1884  cbvex2  1969  dvelimALT  2061  dvelimfv  2062  dvelimor  2069  nfeuv  2095  moaneu  2154  moanmo  2155  eqeltri  2302  nfcxfr  2369  neir  2403  neirr  2409  eqnetri  2423  nesymir  2447  nelir  2498  mprgbir  2588  vex  2802  issetri  2809  moeq  2978  cdeqi  3013  ru  3027  eqsstri  3256  3sstr4i  3265  mosn  3702  rabrsndc  3734  tpid1  3777  tpid2  3779  tpid3  3782  pwv  3886  uni0  3914  eqbrtri  4103  tr0  4192  trv  4193  zfnuleu  4207  0ex  4210  inex1  4217  elpwi2  4241  0elpw  4247  axpow2  4259  axpow3  4260  vpwex  4262  zfpair2  4293  exss  4312  opwo0id  4334  moop2  4337  pwundifss  4375  po0  4401  epse  4432  fr0  4441  0elon  4482  onm  4491  uniex2  4526  snnex  4538  ordtriexmidlem  4610  ordtriexmid  4612  ontr2exmid  4616  ordtri2or2exmidlem  4617  onsucsssucexmid  4618  onsucelsucexmidlem  4620  ruALT  4642  zfregfr  4665  dcextest  4672  zfinf2  4680  omex  4684  finds  4691  finds2  4692  ordom  4698  omsinds  4713  relsnop  4824  relxp  4827  rel0  4843  relopabiv  4844  relopabi  4846  eliunxp  4860  opeliunxp2  4861  dmi  4937  xpidtr  5118  cnvcnv  5180  dmsn0  5195  cnvsn0  5196  funmpt  5355  funmpt2  5356  funinsn  5369  isarep2  5407  f0  5515  f10  5605  f10d  5606  f1o00  5607  f1oi  5610  f1osn  5612  brprcneu  5619  fvopab3ig  5707  opabex  5862  eufnfv  5869  mpofun  6105  reldmmpo  6115  ovid  6120  ovidig  6121  ovidi  6122  ovig  6125  ovi3  6141  oprabex  6271  oprabex3  6272  f1stres  6303  f2ndres  6304  opeliunxp2f  6382  tpos0  6418  issmo  6432  tfrlem6  6460  tfrlem8  6462  tfri1dALT  6495  tfrcl  6508  rdgfun  6517  frecfun  6539  frecfcllem  6548  0lt1o  6584  eqer  6710  ecopover  6778  ecopoverg  6781  th3qcor  6784  mapsnf1o3  6842  ssdomg  6928  ensn1  6946  xpcomf1o  6980  fiunsnnn  7039  finexdc  7060  exmidpw  7066  dcfi  7144  omct  7280  infnninf  7287  infnninfOLD  7288  pm54.43  7359  exmidonfinlem  7367  pw1on  7407  pw1dom2  7408  pw1ne1  7410  2oneel  7438  dmaddpi  7508  dmmulpi  7509  1lt2pi  7523  indpi  7525  1lt2nq  7589  genpelxp  7694  ltexprlempr  7791  recexprlempr  7815  cauappcvgprlemcl  7836  cauappcvgprlemladd  7841  caucvgprlemcl  7859  caucvgprprlemcl  7887  m1p1sr  7943  m1m1sr  7944  0lt1sr  7948  peano1nnnn  8035  ax1cn  8044  ax1re  8045  axaddf  8051  axmulf  8052  ax0lt1  8059  0lt1  8269  subaddrii  8431  ixi  8726  1ap0  8733  sup3exmid  9100  nn1suc  9125  neg1lt0  9214  4d2e2  9267  iap0  9330  un0mulcl  9399  pnf0xnn0  9435  3halfnz  9540  nummac  9618  uzf  9721  mnfltpnf  9977  ixxf  10090  ioof  10163  fzf  10204  fzp1disj  10272  fzp1nel  10296  fzo0  10362  frecfzennn  10643  frechashgf1o  10645  xnn0nnen  10654  fxnn0nninf  10656  seq3f1olemp  10732  sq0  10847  irec  10856  hash0  11013  prhash2ex  11026  climmo  11804  sum0  11894  fisumcom2  11944  prod0  12091  fprodcom2fi  12132  cos1bnd  12265  cos2bnd  12266  3dvds  12370  n2dvdsm1  12419  n2dvds3  12421  flodddiv4  12442  3lcm2e6woprm  12603  6lcm4e12  12604  2prm  12644  3lcm2e6  12677  pockthi  12876  modsubi  12937  unennn  12963  ssnnctlemct  13012  structcnvcnv  13043  strleun  13132  starvndxnbasendx  13170  starvndxnplusgndx  13171  starvndxnmulrndx  13172  scandxnbasendx  13182  scandxnplusgndx  13183  scandxnmulrndx  13184  vscandxnbasendx  13187  vscandxnplusgndx  13188  vscandxnmulrndx  13189  vscandxnscandx  13190  ipndxnbasendx  13200  ipndxnplusgndx  13201  ipndxnmulrndx  13202  slotsdifipndx  13203  tsetndxnplusgndx  13220  tsetndxnmulrndx  13221  tsetndxnstarvndx  13222  slotstnscsi  13223  plendxnplusgndx  13234  plendxnmulrndx  13235  plendxnscandx  13236  plendxnvscandx  13237  slotsdifplendx  13238  basendxnocndx  13241  plendxnocndx  13242  dsndxnplusgndx  13249  dsndxnmulrndx  13250  slotsdnscsi  13251  dsndxntsetndx  13252  slotsdifdsndx  13253  unifndxntsetndx  13259  slotsdifunifndx  13260  restid  13278  prdsval  13301  mgmidmo  13400  rrgmex  14219  lssmex  14313  lidlmex  14433  2idlmex  14459  fczpsrbag  14629  tgdom  14740  tgidm  14742  resttopon  14839  rest0  14847  psmetrel  14990  metrel  15010  xmetrel  15011  xmetf  15018  0met  15052  mopnrel  15109  setsmsbasg  15147  setsmsdsg  15148  qtopbasss  15189  reldvg  15347  dvexp  15379  dveflem  15394  elply2  15403  elplyd  15409  ply1term  15411  plymullem  15418  efcn  15436  sinhalfpilem  15459  sincosq1lem  15493  tangtx  15506  sincos4thpi  15508  pigt3  15512  dfrelog  15528  relogf1o  15529  log1  15534  loge  15535  relogiso  15541  2logb9irr  15639  2logb9irrap  15645  2sqlem9  15797  2sqlem10  15798  uhgr0e  15876  uhgr0  15879  umgrbien  15904  ex-fl  16047  bj-nndcALT  16080  bj-axempty  16214  bj-axempty2  16215  bdinex1  16220  bj-zfpair2  16231  bj-uniex2  16237  bj-indint  16252  bj-omind  16255  bj-omex  16263  bj-omelon  16282  0nninf  16329  dceqnconst  16387  dcapnconst  16388