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  692  stabnot  834  mpbir2an  944  mpbir3an  1181  tru  1368  dcfromnotnotr  1458  dcfromcon  1459  dcfrompeirce  1460  mpgbir  1467  nfxfr  1488  19.8a  1604  sbt  1798  dveeq2  1829  dveeq2or  1830  sbequilem  1852  cbvex2  1937  dvelimALT  2029  dvelimfv  2030  dvelimor  2037  nfeuv  2063  moaneu  2121  moanmo  2122  eqeltri  2269  nfcxfr  2336  neir  2370  neirr  2376  eqnetri  2390  nesymir  2414  nelir  2465  mprgbir  2555  vex  2766  issetri  2772  moeq  2939  cdeqi  2974  ru  2988  eqsstri  3216  3sstr4i  3225  mosn  3659  rabrsndc  3691  tpid1  3734  tpid2  3736  tpid3  3739  pwv  3839  uni0  3867  eqbrtri  4055  tr0  4143  trv  4144  zfnuleu  4158  0ex  4161  inex1  4168  elpwi2  4192  0elpw  4198  axpow2  4210  axpow3  4211  vpwex  4213  zfpair2  4244  exss  4261  moop2  4285  pwundifss  4321  po0  4347  epse  4378  fr0  4387  0elon  4428  onm  4437  uniex2  4472  snnex  4484  ordtriexmidlem  4556  ordtriexmid  4558  ontr2exmid  4562  ordtri2or2exmidlem  4563  onsucsssucexmid  4564  onsucelsucexmidlem  4566  ruALT  4588  zfregfr  4611  dcextest  4618  zfinf2  4626  omex  4630  finds  4637  finds2  4638  ordom  4644  omsinds  4659  relsnop  4770  relxp  4773  rel0  4789  relopabiv  4790  relopabi  4792  eliunxp  4806  opeliunxp2  4807  dmi  4882  xpidtr  5061  cnvcnv  5123  dmsn0  5138  cnvsn0  5139  funmpt  5297  funmpt2  5298  funinsn  5308  isarep2  5346  f0  5451  f10  5541  f1o00  5542  f1oi  5545  f1osn  5547  brprcneu  5554  fvopab3ig  5638  opabex  5789  eufnfv  5796  mpofun  6028  reldmmpo  6038  ovid  6043  ovidig  6044  ovidi  6045  ovig  6048  ovi3  6064  oprabex  6194  oprabex3  6195  f1stres  6226  f2ndres  6227  opeliunxp2f  6305  tpos0  6341  issmo  6355  tfrlem6  6383  tfrlem8  6385  tfri1dALT  6418  tfrcl  6431  rdgfun  6440  frecfun  6462  frecfcllem  6471  0lt1o  6507  eqer  6633  ecopover  6701  ecopoverg  6704  th3qcor  6707  mapsnf1o3  6765  ssdomg  6846  ensn1  6864  xpcomf1o  6893  fiunsnnn  6951  finexdc  6972  exmidpw  6978  dcfi  7056  omct  7192  infnninf  7199  infnninfOLD  7200  pm54.43  7271  exmidonfinlem  7274  pw1on  7311  pw1dom2  7312  pw1ne1  7314  2oneel  7341  dmaddpi  7411  dmmulpi  7412  1lt2pi  7426  indpi  7428  1lt2nq  7492  genpelxp  7597  ltexprlempr  7694  recexprlempr  7718  cauappcvgprlemcl  7739  cauappcvgprlemladd  7744  caucvgprlemcl  7762  caucvgprprlemcl  7790  m1p1sr  7846  m1m1sr  7847  0lt1sr  7851  peano1nnnn  7938  ax1cn  7947  ax1re  7948  axaddf  7954  axmulf  7955  ax0lt1  7962  0lt1  8172  subaddrii  8334  ixi  8629  1ap0  8636  sup3exmid  9003  nn1suc  9028  neg1lt0  9117  4d2e2  9170  iap0  9233  un0mulcl  9302  pnf0xnn0  9338  3halfnz  9442  nummac  9520  uzf  9623  mnfltpnf  9879  ixxf  9992  ioof  10065  fzf  10106  fzp1disj  10174  fzp1nel  10198  fzo0  10263  frecfzennn  10537  frechashgf1o  10539  xnn0nnen  10548  fxnn0nninf  10550  seq3f1olemp  10626  sq0  10741  irec  10750  hash0  10907  prhash2ex  10920  climmo  11482  sum0  11572  fisumcom2  11622  prod0  11769  fprodcom2fi  11810  cos1bnd  11943  cos2bnd  11944  3dvds  12048  n2dvdsm1  12097  n2dvds3  12099  flodddiv4  12120  3lcm2e6woprm  12281  6lcm4e12  12282  2prm  12322  3lcm2e6  12355  pockthi  12554  modsubi  12615  unennn  12641  ssnnctlemct  12690  structcnvcnv  12721  strleun  12809  starvndxnbasendx  12846  starvndxnplusgndx  12847  starvndxnmulrndx  12848  scandxnbasendx  12858  scandxnplusgndx  12859  scandxnmulrndx  12860  vscandxnbasendx  12863  vscandxnplusgndx  12864  vscandxnmulrndx  12865  vscandxnscandx  12866  ipndxnbasendx  12876  ipndxnplusgndx  12877  ipndxnmulrndx  12878  slotsdifipndx  12879  tsetndxnplusgndx  12896  tsetndxnmulrndx  12897  tsetndxnstarvndx  12898  slotstnscsi  12899  plendxnplusgndx  12910  plendxnmulrndx  12911  plendxnscandx  12912  plendxnvscandx  12913  slotsdifplendx  12914  basendxnocndx  12917  plendxnocndx  12918  dsndxnplusgndx  12925  dsndxnmulrndx  12926  slotsdnscsi  12927  dsndxntsetndx  12928  slotsdifdsndx  12929  unifndxntsetndx  12935  slotsdifunifndx  12936  restid  12954  prdsval  12977  mgmidmo  13076  rrgmex  13895  lssmex  13989  lidlmex  14109  2idlmex  14135  fczpsrbag  14305  tgdom  14416  tgidm  14418  resttopon  14515  rest0  14523  psmetrel  14666  metrel  14686  xmetrel  14687  xmetf  14694  0met  14728  mopnrel  14785  setsmsbasg  14823  setsmsdsg  14824  qtopbasss  14865  reldvg  15023  dvexp  15055  dveflem  15070  elply2  15079  elplyd  15085  ply1term  15087  plymullem  15094  efcn  15112  sinhalfpilem  15135  sincosq1lem  15169  tangtx  15182  sincos4thpi  15184  pigt3  15188  dfrelog  15204  relogf1o  15205  log1  15210  loge  15211  relogiso  15217  2logb9irr  15315  2logb9irrap  15321  2sqlem9  15473  2sqlem10  15474  ex-fl  15479  bj-nndcALT  15512  bj-axempty  15647  bj-axempty2  15648  bdinex1  15653  bj-zfpair2  15664  bj-uniex2  15670  bj-indint  15685  bj-omind  15688  bj-omex  15696  bj-omelon  15715  0nninf  15759  dceqnconst  15817  dcapnconst  15818