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  8454  subaddrii  8616  ixi  8913  1ap0  8920  sup3exmid  9289  indconst0  9304  nn1suc  9325  neg1lt0  9414  4d2e2  9469  iap0  9532  un0mulcl  9601  pnf0xnn0  9641  3halfnz  9747  nummac  9830  uzf  9933  mnfltpnf  10197  ixxf  10310  ioof  10383  fzf  10425  fzp1disj  10497  fzp1nel  10521  fzo0  10587  frecfzennn  10876  frechashgf1o  10878  xnn0nnen  10887  fxnn0nninf  10889  seq3f1olemp  10965  sq0  11080  irec  11089  hash0  11249  prhash2ex  11264  hashfibclem  11296  hashf1lem1  11299  climmo  12080  sum0  12171  fisumcom2  12221  prod0  12368  fprodcom2fi  12409  cos1bnd  12542  cos2bnd  12543  3dvds  12647  n2dvdsm1  12696  n2dvds3  12698  flodddiv4  12719  3lcm2e6woprm  12880  6lcm4e12  12881  2prm  12921  3lcm2e6  12955  pockthi  13157  mod2xnegi  13218  modsubi  13219  ballotfilemcdc  13272  ballotfilem2  13277  ballotfilemic  13299  ballotfilem7  13328  ballotfilemth  13330  unennn  13337  ssnnctlemct  13386  structcnvcnv  13417  strleun  13507  starvndxnbasendx  13545  starvndxnplusgndx  13546  starvndxnmulrndx  13547  scandxnbasendx  13557  scandxnplusgndx  13558  scandxnmulrndx  13559  vscandxnbasendx  13562  vscandxnplusgndx  13563  vscandxnmulrndx  13564  vscandxnscandx  13565  ipndxnbasendx  13575  ipndxnplusgndx  13576  ipndxnmulrndx  13577  slotsdifipndx  13578  tsetndxnplusgndx  13595  tsetndxnmulrndx  13596  tsetndxnstarvndx  13597  slotstnscsi  13598  plendxnplusgndx  13609  plendxnmulrndx  13610  plendxnscandx  13611  plendxnvscandx  13612  slotsdifplendx  13613  basendxnocndx  13616  plendxnocndx  13617  dsndxnplusgndx  13624  dsndxnmulrndx  13625  slotsdnscsi  13626  dsndxntsetndx  13627  slotsdifdsndx  13628  unifndxntsetndx  13634  slotsdifunifndx  13635  restid  13653  mgmidmo  13741  gsum0cmn  14203  prdsval  14222  mgpplusg  14271  ringidval  14314  opprringb  14435  reldvdsr  14447  rrgmex  14618  lssmex  14741  lidlmex  14861  2idlmex  14887  asclfval  15070  fczpsrbag  15105  tgdom  15222  tgidm  15224  resttopon  15321  rest0  15329  psmetrel  15472  metrel  15492  xmetrel  15493  xmetf  15500  0met  15534  mopnrel  15591  setsmsbasg  15629  setsmsdsg  15630  qtopbasss  15671  reldvg  15829  dvexp  15861  dveflem  15876  elply2  15885  elplyd  15891  ply1term  15893  plymullem  15900  efcn  15918  sinhalfpilem  15942  sincosq1lem  15976  tangtx  15989  sincos4thpi  15991  pigt3  15995  dfrelog  16011  relogf1o  16012  log1  16017  loge  16018  relogiso  16025  2logb9irr  16126  2logb9irrap  16132  log2ublem1  16140  birthdaylog2  16147  ppiqltx  16183  ppiublem1  16192  ppiqub  16194  bclbnd  16205  bpos1lem  16207  2sqlem9  16341  2sqlem10  16342  uhgr0e  16421  uhgr0  16424  umgrbien  16449  usgr0  16578  griedg0prc  16589  1loopgruspgr  16642  konigsbergumgr  16826  konigsberglem1  16827  ex-fl  16837  bj-nndcALT  16884  bj-axempty  17017  bj-axempty2  17018  bdinex1  17023  bj-zfpair2  17034  bj-uniex2  17040  bj-indint  17055  bj-omind  17058  bj-omex  17066  bj-omelon  17085  pw1ndom3  17118  wexmiddifxylem  17143  0nninf  17145  dceqnconst  17208  dcapnconst  17209