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  4242  0elpw  4248  axpow2  4260  axpow3  4261  vpwex  4263  zfpair2  4294  exss  4313  opwo0id  4335  moop2  4338  pwundifss  4376  po0  4402  epse  4433  fr0  4442  0elon  4483  onm  4492  uniex2  4527  snnex  4539  ordtriexmidlem  4611  ordtriexmid  4613  ontr2exmid  4617  ordtri2or2exmidlem  4618  onsucsssucexmid  4619  onsucelsucexmidlem  4621  ruALT  4643  zfregfr  4666  dcextest  4673  zfinf2  4681  omex  4685  finds  4692  finds2  4693  ordom  4699  omsinds  4714  relsnop  4825  relxp  4828  rel0  4844  relopabiv  4845  relopabi  4847  eliunxp  4861  opeliunxp2  4862  dmi  4938  xpidtr  5119  cnvcnv  5181  dmsn0  5196  cnvsn0  5197  funmpt  5356  funmpt2  5357  funinsn  5370  isarep2  5408  f0  5518  f10  5608  f10d  5609  f1o00  5610  f1oi  5613  f1osn  5615  brprcneu  5622  fvopab3ig  5710  opabex  5867  eufnfv  5874  mpofun  6112  reldmmpo  6122  ovid  6127  ovidig  6128  ovidi  6129  ovig  6132  ovi3  6148  relmptopab  6213  oprabex  6279  oprabex3  6280  f1stres  6311  f2ndres  6312  opeliunxp2f  6390  tpos0  6426  issmo  6440  tfrlem6  6468  tfrlem8  6470  tfri1dALT  6503  tfrcl  6516  rdgfun  6525  frecfun  6547  frecfcllem  6556  0lt1o  6594  eqer  6720  ecopover  6788  ecopoverg  6791  th3qcor  6794  mapsnf1o3  6852  ssdomg  6938  ensn1  6956  xpcomf1o  6992  fiunsnnn  7051  finexdc  7072  exmidpw  7078  dcfi  7156  omct  7292  infnninf  7299  infnninfOLD  7300  pm54.43  7371  exmidonfinlem  7379  pw1on  7419  pw1dom2  7420  pw1ne1  7422  2oneel  7450  dmaddpi  7520  dmmulpi  7521  1lt2pi  7535  indpi  7537  1lt2nq  7601  genpelxp  7706  ltexprlempr  7803  recexprlempr  7827  cauappcvgprlemcl  7848  cauappcvgprlemladd  7853  caucvgprlemcl  7871  caucvgprprlemcl  7899  m1p1sr  7955  m1m1sr  7956  0lt1sr  7960  peano1nnnn  8047  ax1cn  8056  ax1re  8057  axaddf  8063  axmulf  8064  ax0lt1  8071  0lt1  8281  subaddrii  8443  ixi  8738  1ap0  8745  sup3exmid  9112  nn1suc  9137  neg1lt0  9226  4d2e2  9279  iap0  9342  un0mulcl  9411  pnf0xnn0  9447  3halfnz  9552  nummac  9630  uzf  9733  mnfltpnf  9989  ixxf  10102  ioof  10175  fzf  10216  fzp1disj  10284  fzp1nel  10308  fzo0  10374  frecfzennn  10656  frechashgf1o  10658  xnn0nnen  10667  fxnn0nninf  10669  seq3f1olemp  10745  sq0  10860  irec  10869  hash0  11026  prhash2ex  11039  climmo  11817  sum0  11907  fisumcom2  11957  prod0  12104  fprodcom2fi  12145  cos1bnd  12278  cos2bnd  12279  3dvds  12383  n2dvdsm1  12432  n2dvds3  12434  flodddiv4  12455  3lcm2e6woprm  12616  6lcm4e12  12617  2prm  12657  3lcm2e6  12690  pockthi  12889  modsubi  12950  unennn  12976  ssnnctlemct  13025  structcnvcnv  13056  strleun  13145  starvndxnbasendx  13183  starvndxnplusgndx  13184  starvndxnmulrndx  13185  scandxnbasendx  13195  scandxnplusgndx  13196  scandxnmulrndx  13197  vscandxnbasendx  13200  vscandxnplusgndx  13201  vscandxnmulrndx  13202  vscandxnscandx  13203  ipndxnbasendx  13213  ipndxnplusgndx  13214  ipndxnmulrndx  13215  slotsdifipndx  13216  tsetndxnplusgndx  13233  tsetndxnmulrndx  13234  tsetndxnstarvndx  13235  slotstnscsi  13236  plendxnplusgndx  13247  plendxnmulrndx  13248  plendxnscandx  13249  plendxnvscandx  13250  slotsdifplendx  13251  basendxnocndx  13254  plendxnocndx  13255  dsndxnplusgndx  13262  dsndxnmulrndx  13263  slotsdnscsi  13264  dsndxntsetndx  13265  slotsdifdsndx  13266  unifndxntsetndx  13272  slotsdifunifndx  13273  restid  13291  prdsval  13314  mgmidmo  13413  reldvdsr  14063  rrgmex  14233  lssmex  14327  lidlmex  14447  2idlmex  14473  fczpsrbag  14643  tgdom  14754  tgidm  14756  resttopon  14853  rest0  14861  psmetrel  15004  metrel  15024  xmetrel  15025  xmetf  15032  0met  15066  mopnrel  15123  setsmsbasg  15161  setsmsdsg  15162  qtopbasss  15203  reldvg  15361  dvexp  15393  dveflem  15408  elply2  15417  elplyd  15423  ply1term  15425  plymullem  15432  efcn  15450  sinhalfpilem  15473  sincosq1lem  15507  tangtx  15520  sincos4thpi  15522  pigt3  15526  dfrelog  15542  relogf1o  15543  log1  15548  loge  15549  relogiso  15555  2logb9irr  15653  2logb9irrap  15659  2sqlem9  15811  2sqlem10  15812  uhgr0e  15890  uhgr0  15893  umgrbien  15918  ex-fl  16113  bj-nndcALT  16146  bj-axempty  16280  bj-axempty2  16281  bdinex1  16286  bj-zfpair2  16297  bj-uniex2  16303  bj-indint  16318  bj-omind  16321  bj-omex  16329  bj-omelon  16348  pw1ndom3  16383  0nninf  16400  dceqnconst  16458  dcapnconst  16459