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  7458  infnninf  7465  infnninfOLD  7466  pm54.43  7537  exmidonfinlem  7546  pw1on  7586  pw1dom2  7587  pw1ne1  7589  2oneel  7623  dmaddpi  7693  dmmulpi  7694  1lt2pi  7708  indpi  7710  1lt2nq  7774  genpelxp  7879  ltexprlempr  7976  recexprlempr  8000  cauappcvgprlemcl  8021  cauappcvgprlemladd  8026  caucvgprlemcl  8044  caucvgprprlemcl  8072  m1p1sr  8128  m1m1sr  8129  0lt1sr  8133  peano1nnnn  8220  ax1cn  8229  ax1re  8230  axaddf  8236  axmulf  8237  ax0lt1  8244  0lt1  8455  subaddrii  8617  ixi  8914  1ap0  8921  sup3exmid  9290  indconst0  9305  nn1suc  9326  neg1lt0  9415  4d2e2  9470  iap0  9533  un0mulcl  9602  pnf0xnn0  9642  3halfnz  9748  nummac  9831  uzf  9934  mnfltpnf  10198  ixxf  10311  ioof  10384  fzf  10426  fzp1disj  10498  fzp1nel  10522  fzo0  10588  frecfzennn  10878  frechashgf1o  10880  xnn0nnen  10889  fxnn0nninf  10891  seq3f1olemp  10967  sq0  11082  irec  11091  hash0  11251  prhash2ex  11266  hashfibclem  11298  hashf1lem1  11301  climmo  12083  sum0  12174  fisumcom2  12224  prod0  12371  fprodcom2fi  12412  cos1bnd  12545  cos2bnd  12546  3dvds  12650  n2dvdsm1  12699  n2dvds3  12701  flodddiv4  12722  3lcm2e6woprm  12883  6lcm4e12  12884  2prm  12924  3lcm2e6  12958  pockthi  13160  mod2xnegi  13221  modsubi  13222  ballotfilemcdc  13275  ballotfilem2  13280  ballotfilemic  13302  ballotfilem7  13331  ballotfilemth  13333  unennn  13340  ssnnctlemct  13389  structcnvcnv  13420  strleun  13511  starvndxnbasendx  13549  starvndxnplusgndx  13550  starvndxnmulrndx  13551  scandxnbasendx  13561  scandxnplusgndx  13562  scandxnmulrndx  13563  vscandxnbasendx  13566  vscandxnplusgndx  13567  vscandxnmulrndx  13568  vscandxnscandx  13569  ipndxnbasendx  13579  ipndxnplusgndx  13580  ipndxnmulrndx  13581  slotsdifipndx  13582  tsetndxnplusgndx  13599  tsetndxnmulrndx  13600  tsetndxnstarvndx  13601  slotstnscsi  13602  plendxnplusgndx  13613  plendxnmulrndx  13614  plendxnscandx  13615  plendxnvscandx  13616  slotsdifplendx  13617  basendxnocndx  13620  plendxnocndx  13621  dsndxnplusgndx  13628  dsndxnmulrndx  13629  slotsdnscsi  13630  dsndxntsetndx  13631  slotsdifdsndx  13632  unifndxntsetndx  13638  slotsdifunifndx  13639  restid  13657  mgmidmo  13745  gsum0cmn  14238  prdsval  14257  mgpplusg  14306  ringidval  14349  opprringb  14470  reldvdsr  14482  rrgmex  14653  lssmex  14776  lidlmex  14896  2idlmex  14922  asclfval  15105  fczpsrbag  15140  tgdom  15264  tgidm  15266  resttopon  15363  rest0  15371  psmetrel  15514  metrel  15534  xmetrel  15535  xmetf  15542  0met  15576  mopnrel  15633  setsmsbasg  15671  setsmsdsg  15672  qtopbasss  15713  reldvg  15871  dvexp  15903  dveflem  15918  elply2  15927  elplyd  15933  ply1term  15935  plymullem  15942  efcn  15960  sinhalfpilem  15984  sincosq1lem  16018  tangtx  16031  sincos4thpi  16033  pigt3  16037  dfrelog  16053  relogf1o  16054  log1  16059  loge  16060  relogiso  16067  2logb9irr  16168  2logb9irrap  16174  log2ublem1  16182  birthdaylog2  16189  ppiqltx  16242  ppiublem1  16252  ppiqub  16254  bclbnd  16268  bpos1lem  16270  bposlem8  16279  2sqlem9  16409  2sqlem10  16410  uhgr0e  16489  uhgr0  16492  umgrbien  16517  usgr0  16646  griedg0prc  16657  1loopgruspgr  16710  konigsbergumgr  16894  konigsberglem1  16895  ex-fl  16905  bj-nndcALT  16952  bj-axempty  17085  bj-axempty2  17086  bdinex1  17091  bj-zfpair2  17102  bj-uniex2  17108  bj-indint  17123  bj-omind  17126  bj-omex  17134  bj-omelon  17153  pw1ndom3  17186  wexmiddifxylem  17211  0nninf  17213  dceqnconst  17277  dcapnconst  17278