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

This proof depends on syntax axioms:   <-> wb 105

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This proof depends on definitions:  df-bi 117

This theorem is used by:  pm5.74ri  181  imnani  702  stabnot  845  mpbir2an  955  mpbir3an  1210  tru  1406  dcfromnotnotr  1497  dcfromcon  1498  dcfrompeirce  1499  mpgbir  1506  nfxfr  1527  19.8a  1643  sbt  1837  dveeq2  1868  dveeq2or  1869  sbequilem  1891  cbvex2  1978  dvelimALT  2070  dvelimfv  2071  dvelimor  2078  nfeuv  2104  moaneu  2163  moanmo  2164  eqeltri  2311  nfcxfr  2389  neir  2423  neirr  2429  eqnetri  2443  nesymir  2467  nelir  2518  mprgbir  2608  vex  2824  issetri  2831  moeq  3001  cdeqi  3036  ru  3050  eqsstri  3280  3sstr4i  3289  mosn  3745  rabrsndc  3779  tpid1  3824  tpid2  3826  tpid3  3829  pwv  3934  uni0  3962  eqbrtri  4151  tr0  4240  trv  4241  zfnuleu  4257  0ex  4260  inex1  4267  elpwi2  4294  0elpw  4301  axpow2  4313  axpow3  4314  vpwex  4316  zfpair2  4347  exss  4367  opwo0id  4389  moop2  4392  pwundifss  4430  po0  4456  epse  4487  fr0  4496  0elon  4537  onm  4546  uniex2  4581  uniex2OLD  4582  snnex  4594  ordtriexmidlem  4666  ordtriexmid  4668  ontr2exmid  4672  ordtri2or2exmidlem  4673  onsucsssucexmid  4674  onsucelsucexmidlem  4676  ruALT  4698  zfregfr  4721  dcextest  4728  zfinf2  4736  omex  4740  finds  4747  finds2  4748  ordom  4754  omsinds  4769  relsnop  4881  relxp  4884  rel0  4902  relopabiv  4903  relopabi  4905  eliunxp  4919  opeliunxp2  4920  dmi  4996  xpidtr  5178  cnvcnv  5240  dmsn0  5255  cnvsn0  5256  funmpt  5415  funmpt2  5416  funinsn  5430  isarep2  5468  f0  5583  f10  5674  f10d  5675  f1o00  5676  f1oi  5679  f1osn  5681  brprcneu  5688  fvopab3ig  5779  opabex  5941  eufnfv  5949  rinvf1o  6035  mpofun  6190  reldmmpo  6200  ovid  6205  ovidig  6206  ovidi  6207  ovig  6210  ovi3  6226  relmptopab  6291  oprabex  6361  oprabex3  6362  f1stres  6393  f2ndres  6394  opeliunxp2f  6509  tpos0  6545  issmo  6559  tfrlem6  6587  tfrlem8  6589  tfri1dALT  6622  tfrcl  6635  rdgfun  6644  frecfun  6666  frecfcllem  6675  0lt1o  6713  eqer  6839  ecopover  6907  ecopoverg  6910  th3qcor  6913  mapsnf1o3  6979  ssdomg  7065  ensn1  7083  xpcomf1o  7123  fiunsnnn  7185  finexdc  7207  elssdc  7209  exmidpw  7215  fissfi  7263  dcfi  7315  omct  7457  infnninf  7464  infnninfOLD  7465  pm54.43  7536  exmidonfinlem  7545  pw1on  7585  pw1dom2  7586  pw1ne1  7588  2oneel  7622  dmaddpi  7692  dmmulpi  7693  1lt2pi  7707  indpi  7709  1lt2nq  7773  genpelxp  7878  ltexprlempr  7975  recexprlempr  7999  cauappcvgprlemcl  8020  cauappcvgprlemladd  8025  caucvgprlemcl  8043  caucvgprprlemcl  8071  m1p1sr  8127  m1m1sr  8128  0lt1sr  8132  peano1nnnn  8219  ax1cn  8228  ax1re  8229  axaddf  8235  axmulf  8236  ax0lt1  8243  0lt1  8453  subaddrii  8615  ixi  8911  1ap0  8918  sup3exmid  9287  indconst0  9302  nn1suc  9323  neg1lt0  9412  4d2e2  9465  iap0  9528  un0mulcl  9597  pnf0xnn0  9637  3halfnz  9743  nummac  9821  uzf  9924  mnfltpnf  10187  ixxf  10300  ioof  10373  fzf  10415  fzp1disj  10487  fzp1nel  10511  fzo0  10577  frecfzennn  10863  frechashgf1o  10865  xnn0nnen  10874  fxnn0nninf  10876  seq3f1olemp  10952  sq0  11067  irec  11076  hash0  11235  prhash2ex  11250  hashfibclem  11282  hashf1lem1  11285  climmo  12064  sum0  12155  fisumcom2  12205  prod0  12352  fprodcom2fi  12393  cos1bnd  12526  cos2bnd  12527  3dvds  12631  n2dvdsm1  12680  n2dvds3  12682  flodddiv4  12703  3lcm2e6woprm  12864  6lcm4e12  12865  2prm  12905  3lcm2e6  12938  pockthi  13137  modsubi  13198  ballotfilemcdc  13223  ballotfilem2  13228  ballotfilemic  13250  ballotfilem7  13279  ballotfilemth  13281  unennn  13288  ssnnctlemct  13337  structcnvcnv  13368  strleun  13458  starvndxnbasendx  13496  starvndxnplusgndx  13497  starvndxnmulrndx  13498  scandxnbasendx  13508  scandxnplusgndx  13509  scandxnmulrndx  13510  vscandxnbasendx  13513  vscandxnplusgndx  13514  vscandxnmulrndx  13515  vscandxnscandx  13516  ipndxnbasendx  13526  ipndxnplusgndx  13527  ipndxnmulrndx  13528  slotsdifipndx  13529  tsetndxnplusgndx  13546  tsetndxnmulrndx  13547  tsetndxnstarvndx  13548  slotstnscsi  13549  plendxnplusgndx  13560  plendxnmulrndx  13561  plendxnscandx  13562  plendxnvscandx  13563  slotsdifplendx  13564  basendxnocndx  13567  plendxnocndx  13568  dsndxnplusgndx  13575  dsndxnmulrndx  13576  slotsdnscsi  13577  dsndxntsetndx  13578  slotsdifdsndx  13579  unifndxntsetndx  13585  slotsdifunifndx  13586  restid  13604  mgmidmo  13692  gsum0cmn  14154  prdsval  14173  mgpplusg  14222  ringidval  14265  opprringb  14386  reldvdsr  14398  rrgmex  14569  lssmex  14692  lidlmex  14812  2idlmex  14838  asclfval  15021  fczpsrbag  15056  tgdom  15173  tgidm  15175  resttopon  15272  rest0  15280  psmetrel  15423  metrel  15443  xmetrel  15444  xmetf  15451  0met  15485  mopnrel  15542  setsmsbasg  15580  setsmsdsg  15581  qtopbasss  15622  reldvg  15780  dvexp  15812  dveflem  15827  elply2  15836  elplyd  15842  ply1term  15844  plymullem  15851  efcn  15869  sinhalfpilem  15892  sincosq1lem  15926  tangtx  15939  sincos4thpi  15941  pigt3  15945  dfrelog  15961  relogf1o  15962  log1  15967  loge  15968  relogiso  15974  2logb9irr  16073  2logb9irrap  16079  log2ublem1  16083  birthdaylog2  16090  2sqlem9  16243  2sqlem10  16244  uhgr0e  16323  uhgr0  16326  umgrbien  16351  usgr0  16480  griedg0prc  16491  1loopgruspgr  16544  konigsbergumgr  16728  konigsberglem1  16729  ex-fl  16739  bj-nndcALT  16786  bj-axempty  16919  bj-axempty2  16920  bdinex1  16925  bj-zfpair2  16936  bj-uniex2  16942  bj-indint  16957  bj-omind  16960  bj-omex  16968  bj-omelon  16987  pw1ndom3  17020  wexmiddifxylem  17045  0nninf  17047  dceqnconst  17110  dcapnconst  17111