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  693  stabnot  835  mpbir2an  945  mpbir3an  1182  tru  1377  dcfromnotnotr  1468  dcfromcon  1469  dcfrompeirce  1470  mpgbir  1477  nfxfr  1498  19.8a  1614  sbt  1808  dveeq2  1839  dveeq2or  1840  sbequilem  1862  cbvex2  1947  dvelimALT  2039  dvelimfv  2040  dvelimor  2047  nfeuv  2073  moaneu  2131  moanmo  2132  eqeltri  2279  nfcxfr  2346  neir  2380  neirr  2386  eqnetri  2400  nesymir  2424  nelir  2475  mprgbir  2565  vex  2776  issetri  2782  moeq  2949  cdeqi  2984  ru  2998  eqsstri  3226  3sstr4i  3235  mosn  3670  rabrsndc  3702  tpid1  3745  tpid2  3747  tpid3  3750  pwv  3851  uni0  3879  eqbrtri  4068  tr0  4157  trv  4158  zfnuleu  4172  0ex  4175  inex1  4182  elpwi2  4206  0elpw  4212  axpow2  4224  axpow3  4225  vpwex  4227  zfpair2  4258  exss  4275  opwo0id  4297  moop2  4300  pwundifss  4336  po0  4362  epse  4393  fr0  4402  0elon  4443  onm  4452  uniex2  4487  snnex  4499  ordtriexmidlem  4571  ordtriexmid  4573  ontr2exmid  4577  ordtri2or2exmidlem  4578  onsucsssucexmid  4579  onsucelsucexmidlem  4581  ruALT  4603  zfregfr  4626  dcextest  4633  zfinf2  4641  omex  4645  finds  4652  finds2  4653  ordom  4659  omsinds  4674  relsnop  4785  relxp  4788  rel0  4804  relopabiv  4805  relopabi  4807  eliunxp  4821  opeliunxp2  4822  dmi  4898  xpidtr  5078  cnvcnv  5140  dmsn0  5155  cnvsn0  5156  funmpt  5314  funmpt2  5315  funinsn  5328  isarep2  5366  f0  5473  f10  5563  f1o00  5564  f1oi  5567  f1osn  5569  brprcneu  5576  fvopab3ig  5660  opabex  5815  eufnfv  5822  mpofun  6054  reldmmpo  6064  ovid  6069  ovidig  6070  ovidi  6071  ovig  6074  ovi3  6090  oprabex  6220  oprabex3  6221  f1stres  6252  f2ndres  6253  opeliunxp2f  6331  tpos0  6367  issmo  6381  tfrlem6  6409  tfrlem8  6411  tfri1dALT  6444  tfrcl  6457  rdgfun  6466  frecfun  6488  frecfcllem  6497  0lt1o  6533  eqer  6659  ecopover  6727  ecopoverg  6730  th3qcor  6733  mapsnf1o3  6791  ssdomg  6877  ensn1  6895  xpcomf1o  6927  fiunsnnn  6985  finexdc  7006  exmidpw  7012  dcfi  7090  omct  7226  infnninf  7233  infnninfOLD  7234  pm54.43  7305  exmidonfinlem  7308  pw1on  7345  pw1dom2  7346  pw1ne1  7348  2oneel  7375  dmaddpi  7445  dmmulpi  7446  1lt2pi  7460  indpi  7462  1lt2nq  7526  genpelxp  7631  ltexprlempr  7728  recexprlempr  7752  cauappcvgprlemcl  7773  cauappcvgprlemladd  7778  caucvgprlemcl  7796  caucvgprprlemcl  7824  m1p1sr  7880  m1m1sr  7881  0lt1sr  7885  peano1nnnn  7972  ax1cn  7981  ax1re  7982  axaddf  7988  axmulf  7989  ax0lt1  7996  0lt1  8206  subaddrii  8368  ixi  8663  1ap0  8670  sup3exmid  9037  nn1suc  9062  neg1lt0  9151  4d2e2  9204  iap0  9267  un0mulcl  9336  pnf0xnn0  9372  3halfnz  9477  nummac  9555  uzf  9658  mnfltpnf  9914  ixxf  10027  ioof  10100  fzf  10141  fzp1disj  10209  fzp1nel  10233  fzo0  10299  frecfzennn  10578  frechashgf1o  10580  xnn0nnen  10589  fxnn0nninf  10591  seq3f1olemp  10667  sq0  10782  irec  10791  hash0  10948  prhash2ex  10961  climmo  11653  sum0  11743  fisumcom2  11793  prod0  11940  fprodcom2fi  11981  cos1bnd  12114  cos2bnd  12115  3dvds  12219  n2dvdsm1  12268  n2dvds3  12270  flodddiv4  12291  3lcm2e6woprm  12452  6lcm4e12  12453  2prm  12493  3lcm2e6  12526  pockthi  12725  modsubi  12786  unennn  12812  ssnnctlemct  12861  structcnvcnv  12892  strleun  12980  starvndxnbasendx  13018  starvndxnplusgndx  13019  starvndxnmulrndx  13020  scandxnbasendx  13030  scandxnplusgndx  13031  scandxnmulrndx  13032  vscandxnbasendx  13035  vscandxnplusgndx  13036  vscandxnmulrndx  13037  vscandxnscandx  13038  ipndxnbasendx  13048  ipndxnplusgndx  13049  ipndxnmulrndx  13050  slotsdifipndx  13051  tsetndxnplusgndx  13068  tsetndxnmulrndx  13069  tsetndxnstarvndx  13070  slotstnscsi  13071  plendxnplusgndx  13082  plendxnmulrndx  13083  plendxnscandx  13084  plendxnvscandx  13085  slotsdifplendx  13086  basendxnocndx  13089  plendxnocndx  13090  dsndxnplusgndx  13097  dsndxnmulrndx  13098  slotsdnscsi  13099  dsndxntsetndx  13100  slotsdifdsndx  13101  unifndxntsetndx  13107  slotsdifunifndx  13108  restid  13126  prdsval  13149  mgmidmo  13248  rrgmex  14067  lssmex  14161  lidlmex  14281  2idlmex  14307  fczpsrbag  14477  tgdom  14588  tgidm  14590  resttopon  14687  rest0  14695  psmetrel  14838  metrel  14858  xmetrel  14859  xmetf  14866  0met  14900  mopnrel  14957  setsmsbasg  14995  setsmsdsg  14996  qtopbasss  15037  reldvg  15195  dvexp  15227  dveflem  15242  elply2  15251  elplyd  15257  ply1term  15259  plymullem  15266  efcn  15284  sinhalfpilem  15307  sincosq1lem  15341  tangtx  15354  sincos4thpi  15356  pigt3  15360  dfrelog  15376  relogf1o  15377  log1  15382  loge  15383  relogiso  15389  2logb9irr  15487  2logb9irrap  15493  2sqlem9  15645  2sqlem10  15646  uhgr0e  15722  uhgr0  15725  ex-fl  15735  bj-nndcALT  15768  bj-axempty  15903  bj-axempty2  15904  bdinex1  15909  bj-zfpair2  15920  bj-uniex2  15926  bj-indint  15941  bj-omind  15944  bj-omex  15952  bj-omelon  15971  0nninf  16015  dceqnconst  16073  dcapnconst  16074