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  838  mpbir2an  948  mpbir3an  1203  tru  1399  dcfromnotnotr  1490  dcfromcon  1491  dcfrompeirce  1492  mpgbir  1499  nfxfr  1520  19.8a  1636  sbt  1830  dveeq2  1861  dveeq2or  1862  sbequilem  1884  cbvex2  1969  dvelimALT  2061  dvelimfv  2062  dvelimor  2069  nfeuv  2095  moaneu  2154  moanmo  2155  eqeltri  2302  nfcxfr  2369  neir  2403  neirr  2409  eqnetri  2423  nesymir  2447  nelir  2498  mprgbir  2588  vex  2802  issetri  2809  moeq  2978  cdeqi  3013  ru  3027  eqsstri  3256  3sstr4i  3265  mosn  3702  rabrsndc  3734  tpid1  3778  tpid2  3780  tpid3  3783  pwv  3887  uni0  3915  eqbrtri  4104  tr0  4193  trv  4194  zfnuleu  4208  0ex  4211  inex1  4218  elpwi2  4243  0elpw  4249  axpow2  4261  axpow3  4262  vpwex  4264  zfpair2  4295  exss  4314  opwo0id  4336  moop2  4339  pwundifss  4377  po0  4403  epse  4434  fr0  4443  0elon  4484  onm  4493  uniex2  4528  snnex  4540  ordtriexmidlem  4612  ordtriexmid  4614  ontr2exmid  4618  ordtri2or2exmidlem  4619  onsucsssucexmid  4620  onsucelsucexmidlem  4622  ruALT  4644  zfregfr  4667  dcextest  4674  zfinf2  4682  omex  4686  finds  4693  finds2  4694  ordom  4700  omsinds  4715  relsnop  4827  relxp  4830  rel0  4847  relopabiv  4848  relopabi  4850  eliunxp  4864  opeliunxp2  4865  dmi  4941  xpidtr  5122  cnvcnv  5184  dmsn0  5199  cnvsn0  5200  funmpt  5359  funmpt2  5360  funinsn  5373  isarep2  5411  f0  5521  f10  5611  f10d  5612  f1o00  5613  f1oi  5616  f1osn  5618  brprcneu  5625  fvopab3ig  5713  opabex  5870  eufnfv  5877  mpofun  6115  reldmmpo  6125  ovid  6130  ovidig  6131  ovidi  6132  ovig  6135  ovi3  6151  relmptopab  6216  oprabex  6282  oprabex3  6283  f1stres  6314  f2ndres  6315  opeliunxp2f  6395  tpos0  6431  issmo  6445  tfrlem6  6473  tfrlem8  6475  tfri1dALT  6508  tfrcl  6521  rdgfun  6530  frecfun  6552  frecfcllem  6561  0lt1o  6599  eqer  6725  ecopover  6793  ecopoverg  6796  th3qcor  6799  mapsnf1o3  6857  ssdomg  6943  ensn1  6961  xpcomf1o  6997  fiunsnnn  7056  finexdc  7078  elssdc  7080  exmidpw  7086  dcfi  7164  omct  7300  infnninf  7307  infnninfOLD  7308  pm54.43  7379  exmidonfinlem  7387  pw1on  7427  pw1dom2  7428  pw1ne1  7430  2oneel  7458  dmaddpi  7528  dmmulpi  7529  1lt2pi  7543  indpi  7545  1lt2nq  7609  genpelxp  7714  ltexprlempr  7811  recexprlempr  7835  cauappcvgprlemcl  7856  cauappcvgprlemladd  7861  caucvgprlemcl  7879  caucvgprprlemcl  7907  m1p1sr  7963  m1m1sr  7964  0lt1sr  7968  peano1nnnn  8055  ax1cn  8064  ax1re  8065  axaddf  8071  axmulf  8072  ax0lt1  8079  0lt1  8289  subaddrii  8451  ixi  8746  1ap0  8753  sup3exmid  9120  nn1suc  9145  neg1lt0  9234  4d2e2  9287  iap0  9350  un0mulcl  9419  pnf0xnn0  9455  3halfnz  9560  nummac  9638  uzf  9741  mnfltpnf  9998  ixxf  10111  ioof  10184  fzf  10225  fzp1disj  10293  fzp1nel  10317  fzo0  10383  frecfzennn  10665  frechashgf1o  10667  xnn0nnen  10676  fxnn0nninf  10678  seq3f1olemp  10754  sq0  10869  irec  10878  hash0  11035  prhash2ex  11049  climmo  11830  sum0  11920  fisumcom2  11970  prod0  12117  fprodcom2fi  12158  cos1bnd  12291  cos2bnd  12292  3dvds  12396  n2dvdsm1  12445  n2dvds3  12447  flodddiv4  12468  3lcm2e6woprm  12629  6lcm4e12  12630  2prm  12670  3lcm2e6  12703  pockthi  12902  modsubi  12963  unennn  12989  ssnnctlemct  13038  structcnvcnv  13069  strleun  13158  starvndxnbasendx  13196  starvndxnplusgndx  13197  starvndxnmulrndx  13198  scandxnbasendx  13208  scandxnplusgndx  13209  scandxnmulrndx  13210  vscandxnbasendx  13213  vscandxnplusgndx  13214  vscandxnmulrndx  13215  vscandxnscandx  13216  ipndxnbasendx  13226  ipndxnplusgndx  13227  ipndxnmulrndx  13228  slotsdifipndx  13229  tsetndxnplusgndx  13246  tsetndxnmulrndx  13247  tsetndxnstarvndx  13248  slotstnscsi  13249  plendxnplusgndx  13260  plendxnmulrndx  13261  plendxnscandx  13262  plendxnvscandx  13263  slotsdifplendx  13264  basendxnocndx  13267  plendxnocndx  13268  dsndxnplusgndx  13275  dsndxnmulrndx  13276  slotsdnscsi  13277  dsndxntsetndx  13278  slotsdifdsndx  13279  unifndxntsetndx  13285  slotsdifunifndx  13286  restid  13304  prdsval  13327  mgmidmo  13426  reldvdsr  14076  rrgmex  14246  lssmex  14340  lidlmex  14460  2idlmex  14486  fczpsrbag  14656  tgdom  14767  tgidm  14769  resttopon  14866  rest0  14874  psmetrel  15017  metrel  15037  xmetrel  15038  xmetf  15045  0met  15079  mopnrel  15136  setsmsbasg  15174  setsmsdsg  15175  qtopbasss  15216  reldvg  15374  dvexp  15406  dveflem  15421  elply2  15430  elplyd  15436  ply1term  15438  plymullem  15445  efcn  15463  sinhalfpilem  15486  sincosq1lem  15520  tangtx  15533  sincos4thpi  15535  pigt3  15539  dfrelog  15555  relogf1o  15556  log1  15561  loge  15562  relogiso  15568  2logb9irr  15666  2logb9irrap  15672  2sqlem9  15824  2sqlem10  15825  uhgr0e  15903  uhgr0  15906  umgrbien  15931  usgr0  16058  griedg0prc  16069  ex-fl  16198  bj-nndcALT  16231  bj-axempty  16365  bj-axempty2  16366  bdinex1  16371  bj-zfpair2  16382  bj-uniex2  16388  bj-indint  16403  bj-omind  16406  bj-omex  16414  bj-omelon  16433  pw1ndom3  16467  0nninf  16484  dceqnconst  16542  dcapnconst  16543