Theorem mpbir 145

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 132	. 2 ⊢ (𝜓 → 𝜑)
4	1, 3	ax-mp 5	1 ⊢ 𝜑

Syntax hints:   ↔ wb 104

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  pm5.74ri  180  imnani  680  stabnot  818  mpbir2an  926  mpbir3an  1163  tru  1335  mpgbir  1429  nfxfr  1450  19.8a  1569  sbt  1757  dveeq2  1787  dveeq2or  1788  sbequilem  1810  cbvex2  1892  dvelimALT  1983  dvelimfv  1984  dvelimor  1991  nfeuv  2015  moaneu  2073  moanmo  2074  eqeltri  2210  nfcxfr  2276  neir  2309  neirr  2315  eqnetri  2329  nesymir  2353  nelir  2404  mprgbir  2488  vex  2684  issetri  2690  moeq  2854  cdeqi  2889  ru  2903  eqsstri  3124  3sstr4i  3133  rgenm  3460  mosn  3555  rabrsndc  3586  tpid1  3629  tpid2  3631  tpid3  3634  pwv  3730  uni0  3758  eqbrtri  3944  tr0  4032  trv  4033  zfnuleu  4047  0ex  4050  inex1  4057  0elpw  4083  axpow2  4095  axpow3  4096  vpwex  4098  zfpair2  4127  exss  4144  moop2  4168  pwundifss  4202  po0  4228  epse  4259  fr0  4268  0elon  4309  onm  4318  uniex2  4353  snnex  4364  ordtriexmidlem  4430  ordtriexmid  4432  ontr2exmid  4435  ordtri2or2exmidlem  4436  onsucsssucexmid  4437  onsucelsucexmidlem  4439  ruALT  4461  zfregfr  4483  dcextest  4490  zfinf2  4498  omex  4502  finds  4509  finds2  4510  ordom  4515  omsinds  4530  relsnop  4640  relxp  4643  rel0  4659  relopabi  4660  eliunxp  4673  opeliunxp2  4674  dmi  4749  xpidtr  4924  cnvcnv  4986  dmsn0  5001  cnvsn0  5002  funmpt  5156  funmpt2  5157  funinsn  5167  isarep2  5205  f0  5308  f10  5394  f1o00  5395  f1oi  5398  f1osn  5400  brprcneu  5407  fvopab3ig  5488  opabex  5637  eufnfv  5641  mpofun  5866  reldmmpo  5875  ovid  5880  ovidig  5881  ovidi  5882  ovig  5885  ovi3  5900  oprabex  6019  oprabex3  6020  f1stres  6050  f2ndres  6051  opeliunxp2f  6128  tpos0  6164  issmo  6178  tfrlem6  6206  tfrlem8  6208  tfri1dALT  6241  tfrcl  6254  rdgfun  6263  frecfun  6285  frecfcllem  6294  0lt1o  6330  eqer  6454  ecopover  6520  ecopoverg  6523  th3qcor  6526  mapsnf1o3  6584  ssdomg  6665  ensn1  6683  xpcomf1o  6712  fiunsnnn  6768  finexdc  6789  exmidpw  6795  omct  6995  infnninf  7015  nnnninf  7016  pm54.43  7039  exmidonfinlem  7042  dmaddpi  7126  dmmulpi  7127  1lt2pi  7141  indpi  7143  1lt2nq  7207  genpelxp  7312  ltexprlempr  7409  recexprlempr  7433  cauappcvgprlemcl  7454  cauappcvgprlemladd  7459  caucvgprlemcl  7477  caucvgprprlemcl  7505  m1p1sr  7561  m1m1sr  7562  0lt1sr  7566  peano1nnnn  7653  ax1cn  7662  ax1re  7663  axaddf  7669  axmulf  7670  ax0lt1  7677  0lt1  7882  subaddrii  8044  ixi  8338  1ap0  8345  sup3exmid  8708  nn1suc  8732  neg1lt0  8821  4d2e2  8873  iap0  8936  un0mulcl  9004  pnf0xnn0  9040  3halfnz  9141  nummac  9219  uzf  9322  mnfltpnf  9564  ixxf  9674  ioof  9747  fzf  9787  fzp1disj  9853  fzp1nel  9877  fzo0  9938  frecfzennn  10192  frechashgf1o  10194  fxnn0nninf  10204  seq3f1olemp  10268  sq0  10376  irec  10385  hash0  10536  prhash2ex  10548  climmo  11060  sum0  11150  fisumcom2  11200  cos1bnd  11455  cos2bnd  11456  n2dvdsm1  11599  n2dvds3  11601  flodddiv4  11620  3lcm2e6woprm  11756  6lcm4e12  11757  2prm  11797  3lcm2e6  11827  unennn  11899  structcnvcnv  11964  strleun  12037  restid  12120  tgdom  12230  tgidm  12232  resttopon  12329  rest0  12337  psmetrel  12480  metrel  12500  xmetrel  12501  xmetf  12508  0met  12542  mopnrel  12599  setsmsbasg  12637  setsmsdsg  12638  qtopbasss  12679  reldvg  12806  dvexp  12833  dveflem  12844  efcn  12846  sinhalfpilem  12861  sincosq1lem  12895  tangtx  12908  sincos4thpi  12910  pigt3  12914  ex-fl  12926  bj-nndcALT  12952  bj-axempty  13080  bj-axempty2  13081  bdinex1  13086  bj-zfpair2  13097  bj-uniex2  13103  bj-indint  13118  bj-omind  13121  bj-omex  13129  bj-omelon  13148  pw1dom2  13179  0nninf  13186