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 ⊢ 𝜑

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  837  mpbir2an  947  mpbir3an  1184  tru  1379  dcfromnotnotr  1470  dcfromcon  1471  dcfrompeirce  1472  mpgbir  1479  nfxfr  1500  19.8a  1616  sbt  1810  dveeq2  1841  dveeq2or  1842  sbequilem  1864  cbvex2  1949  dvelimALT  2041  dvelimfv  2042  dvelimor  2049  nfeuv  2075  moaneu  2134  moanmo  2135  eqeltri  2282  nfcxfr  2349  neir  2383  neirr  2389  eqnetri  2403  nesymir  2427  nelir  2478  mprgbir  2568  vex  2782  issetri  2789  moeq  2958  cdeqi  2993  ru  3007  eqsstri  3236  3sstr4i  3245  mosn  3682  rabrsndc  3714  tpid1  3757  tpid2  3759  tpid3  3762  pwv  3866  uni0  3894  eqbrtri  4083  tr0  4172  trv  4173  zfnuleu  4187  0ex  4190  inex1  4197  elpwi2  4221  0elpw  4227  axpow2  4239  axpow3  4240  vpwex  4242  zfpair2  4273  exss  4292  opwo0id  4314  moop2  4317  pwundifss  4353  po0  4379  epse  4410  fr0  4419  0elon  4460  onm  4469  uniex2  4504  snnex  4516  ordtriexmidlem  4588  ordtriexmid  4590  ontr2exmid  4594  ordtri2or2exmidlem  4595  onsucsssucexmid  4596  onsucelsucexmidlem  4598  ruALT  4620  zfregfr  4643  dcextest  4650  zfinf2  4658  omex  4662  finds  4669  finds2  4670  ordom  4676  omsinds  4691  relsnop  4802  relxp  4805  rel0  4821  relopabiv  4822  relopabi  4824  eliunxp  4838  opeliunxp2  4839  dmi  4915  xpidtr  5095  cnvcnv  5157  dmsn0  5172  cnvsn0  5173  funmpt  5332  funmpt2  5333  funinsn  5346  isarep2  5384  f0  5492  f10  5582  f10d  5583  f1o00  5584  f1oi  5587  f1osn  5589  brprcneu  5596  fvopab3ig  5681  opabex  5836  eufnfv  5843  mpofun  6077  reldmmpo  6087  ovid  6092  ovidig  6093  ovidi  6094  ovig  6097  ovi3  6113  oprabex  6243  oprabex3  6244  f1stres  6275  f2ndres  6276  opeliunxp2f  6354  tpos0  6390  issmo  6404  tfrlem6  6432  tfrlem8  6434  tfri1dALT  6467  tfrcl  6480  rdgfun  6489  frecfun  6511  frecfcllem  6520  0lt1o  6556  eqer  6682  ecopover  6750  ecopoverg  6753  th3qcor  6756  mapsnf1o3  6814  ssdomg  6900  ensn1  6918  xpcomf1o  6952  fiunsnnn  7011  finexdc  7032  exmidpw  7038  dcfi  7116  omct  7252  infnninf  7259  infnninfOLD  7260  pm54.43  7331  exmidonfinlem  7339  pw1on  7379  pw1dom2  7380  pw1ne1  7382  2oneel  7410  dmaddpi  7480  dmmulpi  7481  1lt2pi  7495  indpi  7497  1lt2nq  7561  genpelxp  7666  ltexprlempr  7763  recexprlempr  7787  cauappcvgprlemcl  7808  cauappcvgprlemladd  7813  caucvgprlemcl  7831  caucvgprprlemcl  7859  m1p1sr  7915  m1m1sr  7916  0lt1sr  7920  peano1nnnn  8007  ax1cn  8016  ax1re  8017  axaddf  8023  axmulf  8024  ax0lt1  8031  0lt1  8241  subaddrii  8403  ixi  8698  1ap0  8705  sup3exmid  9072  nn1suc  9097  neg1lt0  9186  4d2e2  9239  iap0  9302  un0mulcl  9371  pnf0xnn0  9407  3halfnz  9512  nummac  9590  uzf  9693  mnfltpnf  9949  ixxf  10062  ioof  10135  fzf  10176  fzp1disj  10244  fzp1nel  10268  fzo0  10334  frecfzennn  10615  frechashgf1o  10617  xnn0nnen  10626  fxnn0nninf  10628  seq3f1olemp  10704  sq0  10819  irec  10828  hash0  10985  prhash2ex  10998  climmo  11775  sum0  11865  fisumcom2  11915  prod0  12062  fprodcom2fi  12103  cos1bnd  12236  cos2bnd  12237  3dvds  12341  n2dvdsm1  12390  n2dvds3  12392  flodddiv4  12413  3lcm2e6woprm  12574  6lcm4e12  12575  2prm  12615  3lcm2e6  12648  pockthi  12847  modsubi  12908  unennn  12934  ssnnctlemct  12983  structcnvcnv  13014  strleun  13103  starvndxnbasendx  13141  starvndxnplusgndx  13142  starvndxnmulrndx  13143  scandxnbasendx  13153  scandxnplusgndx  13154  scandxnmulrndx  13155  vscandxnbasendx  13158  vscandxnplusgndx  13159  vscandxnmulrndx  13160  vscandxnscandx  13161  ipndxnbasendx  13171  ipndxnplusgndx  13172  ipndxnmulrndx  13173  slotsdifipndx  13174  tsetndxnplusgndx  13191  tsetndxnmulrndx  13192  tsetndxnstarvndx  13193  slotstnscsi  13194  plendxnplusgndx  13205  plendxnmulrndx  13206  plendxnscandx  13207  plendxnvscandx  13208  slotsdifplendx  13209  basendxnocndx  13212  plendxnocndx  13213  dsndxnplusgndx  13220  dsndxnmulrndx  13221  slotsdnscsi  13222  dsndxntsetndx  13223  slotsdifdsndx  13224  unifndxntsetndx  13230  slotsdifunifndx  13231  restid  13249  prdsval  13272  mgmidmo  13371  rrgmex  14190  lssmex  14284  lidlmex  14404  2idlmex  14430  fczpsrbag  14600  tgdom  14711  tgidm  14713  resttopon  14810  rest0  14818  psmetrel  14961  metrel  14981  xmetrel  14982  xmetf  14989  0met  15023  mopnrel  15080  setsmsbasg  15118  setsmsdsg  15119  qtopbasss  15160  reldvg  15318  dvexp  15350  dveflem  15365  elply2  15374  elplyd  15380  ply1term  15382  plymullem  15389  efcn  15407  sinhalfpilem  15430  sincosq1lem  15464  tangtx  15477  sincos4thpi  15479  pigt3  15483  dfrelog  15499  relogf1o  15500  log1  15505  loge  15506  relogiso  15512  2logb9irr  15610  2logb9irrap  15616  2sqlem9  15768  2sqlem10  15769  uhgr0e  15847  uhgr0  15850  umgrbien  15875  ex-fl  15999  bj-nndcALT  16032  bj-axempty  16166  bj-axempty2  16167  bdinex1  16172  bj-zfpair2  16183  bj-uniex2  16189  bj-indint  16204  bj-omind  16207  bj-omex  16215  bj-omelon  16234  0nninf  16281  dceqnconst  16339  dcapnconst  16340