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  3778  tpid2  3780  tpid3  3783  pwv  3887  uni0  3915  eqbrtri  4104  tr0  4193  trv  4194  zfnuleu  4208  0ex  4211  inex1  4218  elpwi2  4242  0elpw  4248  axpow2  4260  axpow3  4261  vpwex  4263  zfpair2  4294  exss  4313  opwo0id  4335  moop2  4338  pwundifss  4376  po0  4402  epse  4433  fr0  4442  0elon  4483  onm  4492  uniex2  4527  snnex  4539  ordtriexmidlem  4611  ordtriexmid  4613  ontr2exmid  4617  ordtri2or2exmidlem  4618  onsucsssucexmid  4619  onsucelsucexmidlem  4621  ruALT  4643  zfregfr  4666  dcextest  4673  zfinf2  4681  omex  4685  finds  4692  finds2  4693  ordom  4699  omsinds  4714  relsnop  4825  relxp  4828  rel0  4844  relopabiv  4845  relopabi  4847  eliunxp  4861  opeliunxp2  4862  dmi  4938  xpidtr  5119  cnvcnv  5181  dmsn0  5196  cnvsn0  5197  funmpt  5356  funmpt2  5357  funinsn  5370  isarep2  5408  f0  5518  f10  5608  f10d  5609  f1o00  5610  f1oi  5613  f1osn  5615  brprcneu  5622  fvopab3ig  5710  opabex  5867  eufnfv  5874  mpofun  6112  reldmmpo  6122  ovid  6127  ovidig  6128  ovidi  6129  ovig  6132  ovi3  6148  relmptopab  6213  oprabex  6279  oprabex3  6280  f1stres  6311  f2ndres  6312  opeliunxp2f  6390  tpos0  6426  issmo  6440  tfrlem6  6468  tfrlem8  6470  tfri1dALT  6503  tfrcl  6516  rdgfun  6525  frecfun  6547  frecfcllem  6556  0lt1o  6594  eqer  6720  ecopover  6788  ecopoverg  6791  th3qcor  6794  mapsnf1o3  6852  ssdomg  6938  ensn1  6956  xpcomf1o  6992  fiunsnnn  7051  finexdc  7073  elssdc  7075  exmidpw  7081  dcfi  7159  omct  7295  infnninf  7302  infnninfOLD  7303  pm54.43  7374  exmidonfinlem  7382  pw1on  7422  pw1dom2  7423  pw1ne1  7425  2oneel  7453  dmaddpi  7523  dmmulpi  7524  1lt2pi  7538  indpi  7540  1lt2nq  7604  genpelxp  7709  ltexprlempr  7806  recexprlempr  7830  cauappcvgprlemcl  7851  cauappcvgprlemladd  7856  caucvgprlemcl  7874  caucvgprprlemcl  7902  m1p1sr  7958  m1m1sr  7959  0lt1sr  7963  peano1nnnn  8050  ax1cn  8059  ax1re  8060  axaddf  8066  axmulf  8067  ax0lt1  8074  0lt1  8284  subaddrii  8446  ixi  8741  1ap0  8748  sup3exmid  9115  nn1suc  9140  neg1lt0  9229  4d2e2  9282  iap0  9345  un0mulcl  9414  pnf0xnn0  9450  3halfnz  9555  nummac  9633  uzf  9736  mnfltpnf  9993  ixxf  10106  ioof  10179  fzf  10220  fzp1disj  10288  fzp1nel  10312  fzo0  10378  frecfzennn  10660  frechashgf1o  10662  xnn0nnen  10671  fxnn0nninf  10673  seq3f1olemp  10749  sq0  10864  irec  10873  hash0  11030  prhash2ex  11044  climmo  11824  sum0  11914  fisumcom2  11964  prod0  12111  fprodcom2fi  12152  cos1bnd  12285  cos2bnd  12286  3dvds  12390  n2dvdsm1  12439  n2dvds3  12441  flodddiv4  12462  3lcm2e6woprm  12623  6lcm4e12  12624  2prm  12664  3lcm2e6  12697  pockthi  12896  modsubi  12957  unennn  12983  ssnnctlemct  13032  structcnvcnv  13063  strleun  13152  starvndxnbasendx  13190  starvndxnplusgndx  13191  starvndxnmulrndx  13192  scandxnbasendx  13202  scandxnplusgndx  13203  scandxnmulrndx  13204  vscandxnbasendx  13207  vscandxnplusgndx  13208  vscandxnmulrndx  13209  vscandxnscandx  13210  ipndxnbasendx  13220  ipndxnplusgndx  13221  ipndxnmulrndx  13222  slotsdifipndx  13223  tsetndxnplusgndx  13240  tsetndxnmulrndx  13241  tsetndxnstarvndx  13242  slotstnscsi  13243  plendxnplusgndx  13254  plendxnmulrndx  13255  plendxnscandx  13256  plendxnvscandx  13257  slotsdifplendx  13258  basendxnocndx  13261  plendxnocndx  13262  dsndxnplusgndx  13269  dsndxnmulrndx  13270  slotsdnscsi  13271  dsndxntsetndx  13272  slotsdifdsndx  13273  unifndxntsetndx  13279  slotsdifunifndx  13280  restid  13298  prdsval  13321  mgmidmo  13420  reldvdsr  14070  rrgmex  14240  lssmex  14334  lidlmex  14454  2idlmex  14480  fczpsrbag  14650  tgdom  14761  tgidm  14763  resttopon  14860  rest0  14868  psmetrel  15011  metrel  15031  xmetrel  15032  xmetf  15039  0met  15073  mopnrel  15130  setsmsbasg  15168  setsmsdsg  15169  qtopbasss  15210  reldvg  15368  dvexp  15400  dveflem  15415  elply2  15424  elplyd  15430  ply1term  15432  plymullem  15439  efcn  15457  sinhalfpilem  15480  sincosq1lem  15514  tangtx  15527  sincos4thpi  15529  pigt3  15533  dfrelog  15549  relogf1o  15550  log1  15555  loge  15556  relogiso  15562  2logb9irr  15660  2logb9irrap  15666  2sqlem9  15818  2sqlem10  15819  uhgr0e  15897  uhgr0  15900  umgrbien  15925  ex-fl  16144  bj-nndcALT  16177  bj-axempty  16311  bj-axempty2  16312  bdinex1  16317  bj-zfpair2  16328  bj-uniex2  16334  bj-indint  16349  bj-omind  16352  bj-omex  16360  bj-omelon  16379  pw1ndom3  16413  0nninf  16430  dceqnconst  16488  dcapnconst  16489