Theorem mpbir 146

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

Hypotheses

Ref	Expression
mpbir.min	⊢ 𝜓
mpbir.maj	⊢ (𝜑 ↔ 𝜓)

Assertion

Ref	Expression
mpbir	⊢ 𝜑

Proof of Theorem mpbir

Step	Hyp	Ref	Expression
1		mpbir.min	. 2 ⊢ 𝜓
2		mpbir.maj	. . 3 ⊢ (𝜑 ↔ 𝜓)
3	2	biimpri 133	. 2 ⊢ (𝜓 → 𝜑)
4	1, 3	ax-mp 5	1 ⊢ 𝜑

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  8912  1ap0  8919  sup3exmid  9288  indconst0  9303  nn1suc  9324  neg1lt0  9413  4d2e2  9467  iap0  9530  un0mulcl  9599  pnf0xnn0  9639  3halfnz  9745  nummac  9823  uzf  9926  mnfltpnf  10189  ixxf  10302  ioof  10375  fzf  10417  fzp1disj  10489  fzp1nel  10513  fzo0  10579  frecfzennn  10865  frechashgf1o  10867  xnn0nnen  10876  fxnn0nninf  10878  seq3f1olemp  10954  sq0  11069  irec  11078  hash0  11237  prhash2ex  11252  hashfibclem  11284  hashf1lem1  11287  climmo  12066  sum0  12157  fisumcom2  12207  prod0  12354  fprodcom2fi  12395  cos1bnd  12528  cos2bnd  12529  3dvds  12633  n2dvdsm1  12682  n2dvds3  12684  flodddiv4  12705  3lcm2e6woprm  12866  6lcm4e12  12867  2prm  12907  3lcm2e6  12940  pockthi  13139  modsubi  13200  ballotfilemcdc  13225  ballotfilem2  13230  ballotfilemic  13252  ballotfilem7  13281  ballotfilemth  13283  unennn  13290  ssnnctlemct  13339  structcnvcnv  13370  strleun  13460  starvndxnbasendx  13498  starvndxnplusgndx  13499  starvndxnmulrndx  13500  scandxnbasendx  13510  scandxnplusgndx  13511  scandxnmulrndx  13512  vscandxnbasendx  13515  vscandxnplusgndx  13516  vscandxnmulrndx  13517  vscandxnscandx  13518  ipndxnbasendx  13528  ipndxnplusgndx  13529  ipndxnmulrndx  13530  slotsdifipndx  13531  tsetndxnplusgndx  13548  tsetndxnmulrndx  13549  tsetndxnstarvndx  13550  slotstnscsi  13551  plendxnplusgndx  13562  plendxnmulrndx  13563  plendxnscandx  13564  plendxnvscandx  13565  slotsdifplendx  13566  basendxnocndx  13569  plendxnocndx  13570  dsndxnplusgndx  13577  dsndxnmulrndx  13578  slotsdnscsi  13579  dsndxntsetndx  13580  slotsdifdsndx  13581  unifndxntsetndx  13587  slotsdifunifndx  13588  restid  13606  mgmidmo  13694  gsum0cmn  14156  prdsval  14175  mgpplusg  14224  ringidval  14267  opprringb  14388  reldvdsr  14400  rrgmex  14571  lssmex  14694  lidlmex  14814  2idlmex  14840  asclfval  15023  fczpsrbag  15058  tgdom  15175  tgidm  15177  resttopon  15274  rest0  15282  psmetrel  15425  metrel  15445  xmetrel  15446  xmetf  15453  0met  15487  mopnrel  15544  setsmsbasg  15582  setsmsdsg  15583  qtopbasss  15624  reldvg  15782  dvexp  15814  dveflem  15829  elply2  15838  elplyd  15844  ply1term  15846  plymullem  15853  efcn  15871  sinhalfpilem  15895  sincosq1lem  15929  tangtx  15942  sincos4thpi  15944  pigt3  15948  dfrelog  15964  relogf1o  15965  log1  15970  loge  15971  relogiso  15978  2logb9irr  16079  2logb9irrap  16085  log2ublem1  16089  birthdaylog2  16096  bclbnd  16127  2sqlem9  16255  2sqlem10  16256  uhgr0e  16335  uhgr0  16338  umgrbien  16363  usgr0  16492  griedg0prc  16503  1loopgruspgr  16556  konigsbergumgr  16740  konigsberglem1  16741  ex-fl  16751  bj-nndcALT  16798  bj-axempty  16931  bj-axempty2  16932  bdinex1  16937  bj-zfpair2  16948  bj-uniex2  16954  bj-indint  16969  bj-omind  16972  bj-omex  16980  bj-omelon  16999  pw1ndom3  17032  wexmiddifxylem  17057  0nninf  17059  dceqnconst  17122  dcapnconst  17123