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  691  stabnot  833  mpbir2an  942  mpbir3an  1179  tru  1357  mpgbir  1453  nfxfr  1474  19.8a  1590  sbt  1784  dveeq2  1815  dveeq2or  1816  sbequilem  1838  cbvex2  1922  dvelimALT  2010  dvelimfv  2011  dvelimor  2018  nfeuv  2044  moaneu  2102  moanmo  2103  eqeltri  2250  nfcxfr  2316  neir  2350  neirr  2356  eqnetri  2370  nesymir  2394  nelir  2445  mprgbir  2535  vex  2742  issetri  2748  moeq  2914  cdeqi  2949  ru  2963  eqsstri  3189  3sstr4i  3198  rgenm  3527  mosn  3630  rabrsndc  3662  tpid1  3705  tpid2  3707  tpid3  3710  pwv  3810  uni0  3838  eqbrtri  4026  tr0  4114  trv  4115  zfnuleu  4129  0ex  4132  inex1  4139  elpwi2  4160  0elpw  4166  axpow2  4178  axpow3  4179  vpwex  4181  zfpair2  4212  exss  4229  moop2  4253  pwundifss  4287  po0  4313  epse  4344  fr0  4353  0elon  4394  onm  4403  uniex2  4438  snnex  4450  ordtriexmidlem  4520  ordtriexmid  4522  ontr2exmid  4526  ordtri2or2exmidlem  4527  onsucsssucexmid  4528  onsucelsucexmidlem  4530  ruALT  4552  zfregfr  4575  dcextest  4582  zfinf2  4590  omex  4594  finds  4601  finds2  4602  ordom  4608  omsinds  4623  relsnop  4734  relxp  4737  rel0  4753  relopabi  4754  eliunxp  4768  opeliunxp2  4769  dmi  4844  xpidtr  5021  cnvcnv  5083  dmsn0  5098  cnvsn0  5099  funmpt  5256  funmpt2  5257  funinsn  5267  isarep2  5305  f0  5408  f10  5497  f1o00  5498  f1oi  5501  f1osn  5503  brprcneu  5510  fvopab3ig  5592  opabex  5742  eufnfv  5749  mpofun  5979  reldmmpo  5988  ovid  5993  ovidig  5994  ovidi  5995  ovig  5998  ovi3  6013  oprabex  6131  oprabex3  6132  f1stres  6162  f2ndres  6163  opeliunxp2f  6241  tpos0  6277  issmo  6291  tfrlem6  6319  tfrlem8  6321  tfri1dALT  6354  tfrcl  6367  rdgfun  6376  frecfun  6398  frecfcllem  6407  0lt1o  6443  eqer  6569  ecopover  6635  ecopoverg  6638  th3qcor  6641  mapsnf1o3  6699  ssdomg  6780  ensn1  6798  xpcomf1o  6827  fiunsnnn  6883  finexdc  6904  exmidpw  6910  dcfi  6982  omct  7118  infnninf  7124  infnninfOLD  7125  pm54.43  7191  exmidonfinlem  7194  pw1on  7227  pw1dom2  7228  pw1ne1  7230  2oneel  7257  dmaddpi  7326  dmmulpi  7327  1lt2pi  7341  indpi  7343  1lt2nq  7407  genpelxp  7512  ltexprlempr  7609  recexprlempr  7633  cauappcvgprlemcl  7654  cauappcvgprlemladd  7659  caucvgprlemcl  7677  caucvgprprlemcl  7705  m1p1sr  7761  m1m1sr  7762  0lt1sr  7766  peano1nnnn  7853  ax1cn  7862  ax1re  7863  axaddf  7869  axmulf  7870  ax0lt1  7877  0lt1  8086  subaddrii  8248  ixi  8542  1ap0  8549  sup3exmid  8916  nn1suc  8940  neg1lt0  9029  4d2e2  9081  iap0  9144  un0mulcl  9212  pnf0xnn0  9248  3halfnz  9352  nummac  9430  uzf  9533  mnfltpnf  9787  ixxf  9900  ioof  9973  fzf  10014  fzp1disj  10082  fzp1nel  10106  fzo0  10170  frecfzennn  10428  frechashgf1o  10430  fxnn0nninf  10440  seq3f1olemp  10504  sq0  10613  irec  10622  hash0  10778  prhash2ex  10791  climmo  11308  sum0  11398  fisumcom2  11448  prod0  11595  fprodcom2fi  11636  cos1bnd  11769  cos2bnd  11770  n2dvdsm1  11920  n2dvds3  11922  flodddiv4  11941  3lcm2e6woprm  12088  6lcm4e12  12089  2prm  12129  3lcm2e6  12162  pockthi  12358  unennn  12400  ssnnctlemct  12449  structcnvcnv  12480  strleun  12565  starvndxnbasendx  12602  starvndxnplusgndx  12603  starvndxnmulrndx  12604  scandxnbasendx  12614  scandxnplusgndx  12615  scandxnmulrndx  12616  vscandxnbasendx  12619  vscandxnplusgndx  12620  vscandxnmulrndx  12621  vscandxnscandx  12622  ipndxnbasendx  12632  ipndxnplusgndx  12633  ipndxnmulrndx  12634  slotsdifipndx  12635  tsetndxnplusgndx  12652  tsetndxnmulrndx  12653  tsetndxnstarvndx  12654  slotstnscsi  12655  plendxnplusgndx  12666  plendxnmulrndx  12667  plendxnscandx  12668  plendxnvscandx  12669  slotsdifplendx  12670  dsndxnplusgndx  12677  dsndxnmulrndx  12678  slotsdnscsi  12679  dsndxntsetndx  12680  slotsdifdsndx  12681  unifndxntsetndx  12687  slotsdifunifndx  12688  restid  12704  mgmidmo  12796  tgdom  13611  tgidm  13613  resttopon  13710  rest0  13718  psmetrel  13861  metrel  13881  xmetrel  13882  xmetf  13889  0met  13923  mopnrel  13980  setsmsbasg  14018  setsmsdsg  14019  qtopbasss  14060  reldvg  14187  dvexp  14214  dveflem  14226  efcn  14228  sinhalfpilem  14251  sincosq1lem  14285  tangtx  14298  sincos4thpi  14300  pigt3  14304  dfrelog  14320  relogf1o  14321  log1  14326  loge  14327  relogiso  14333  2logb9irr  14428  2logb9irrap  14434  2sqlem9  14510  2sqlem10  14511  ex-fl  14516  bj-nndcALT  14549  bj-axempty  14684  bj-axempty2  14685  bdinex1  14690  bj-zfpair2  14701  bj-uniex2  14707  bj-indint  14722  bj-omind  14725  bj-omex  14733  bj-omelon  14752  0nninf  14792  dceqnconst  14846  dcapnconst  14847