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 ⊢ 𝜑

This proof depends on syntax axioms:   ↔ wb 105

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This proof depends on definitions:  df-bi 117

This theorem is used by:  pm5.74ri  181  imnani  702  stabnot  845  mpbir2an  955  mpbir3an  1210  tru  1406  dcfromnotnotr  1497  dcfromcon  1498  dcfrompeirce  1499  mpgbir  1506  nfxfr  1527  19.8a  1643  sbt  1837  dveeq2  1868  dveeq2or  1869  sbequilem  1891  cbvex2  1978  dvelimALT  2070  dvelimfv  2071  dvelimor  2078  nfeuv  2104  moaneu  2163  moanmo  2164  eqeltri  2311  nfcxfr  2389  neir  2423  neirr  2429  eqnetri  2443  nesymir  2467  nelir  2518  mprgbir  2608  vex  2824  issetri  2831  moeq  3001  cdeqi  3036  ru  3050  eqsstri  3280  3sstr4i  3289  mosn  3745  rabrsndc  3779  tpid1  3824  tpid2  3826  tpid3  3829  pwv  3934  uni0  3962  eqbrtri  4152  tr0  4242  trv  4243  zfnuleu  4259  0ex  4262  inex1  4269  elpwi2  4296  0elpw  4303  axpow2  4315  axpow3  4316  vpwex  4318  zfpair2  4349  exss  4369  opwo0id  4391  moop2  4394  pwundifss  4432  po0  4458  epse  4489  fr0  4498  0elon  4539  onm  4548  uniex2  4583  uniex2OLD  4584  snnex  4596  ordtriexmidlem  4668  ordtriexmid  4670  ontr2exmid  4674  ordtri2or2exmidlem  4675  onsucsssucexmid  4676  onsucelsucexmidlem  4678  ruALT  4700  zfregfr  4723  dcextest  4730  zfinf2  4738  omex  4742  finds  4749  finds2  4750  ordom  4756  omsinds  4771  relsnop  4883  relxp  4886  rel0  4904  relopabiv  4905  relopabi  4907  eliunxp  4921  opeliunxp2  4922  dmi  4998  xpidtr  5181  cnvcnv  5243  dmsn0  5258  cnvsn0  5259  funmpt  5418  funmpt2  5419  funinsn  5433  isarep2  5471  f0  5586  f10  5677  f10d  5678  f1o00  5679  f1oi  5682  f1osn  5684  brprcneu  5691  fvopab3ig  5782  opabex  5944  eufnfv  5952  rinvf1o  6038  mpofun  6193  reldmmpo  6203  ovid  6208  ovidig  6209  ovidi  6210  ovig  6213  ovi3  6229  relmptopab  6294  oprabex  6365  oprabex3  6366  f1stres  6397  f2ndres  6398  opeliunxp2f  6513  tpos0  6549  issmo  6563  tfrlem6  6591  tfrlem8  6593  tfri1dALT  6626  tfrcl  6639  rdgfun  6648  frecfun  6670  frecfcllem  6679  0lt1o  6717  eqer  6843  ecopover  6911  ecopoverg  6914  th3qcor  6917  mapsnf1o3  6984  ssdomg  7070  ensn1  7088  xpcomf1o  7128  fiunsnnn  7190  finexdc  7212  elssdc  7214  exmidpw  7220  fissfi  7268  dcfi  7321  omct  7464  infnninf  7471  infnninfOLD  7472  pm54.43  7543  exmidonfinlem  7552  pw1on  7592  pw1dom2  7593  pw1ne1  7595  2oneel  7629  dmaddpi  7699  dmmulpi  7700  1lt2pi  7714  indpi  7716  1lt2nq  7780  genpelxp  7885  ltexprlempr  7982  recexprlempr  8006  cauappcvgprlemcl  8027  cauappcvgprlemladd  8032  caucvgprlemcl  8050  caucvgprprlemcl  8078  m1p1sr  8134  m1m1sr  8135  0lt1sr  8139  peano1nnnn  8226  ax1cn  8235  ax1re  8236  axaddf  8242  axmulf  8243  ax0lt1  8250  0lt1  8461  subaddrii  8623  ixi  8920  1ap0  8927  sup3exmid  9296  indconst0  9312  nn1suc  9333  neg1lt0  9422  4d2e2  9477  iap0  9540  un0mulcl  9609  pnf0xnn0  9649  3halfnz  9755  nummac  9838  uzf  9941  mnfltpnf  10205  ixxf  10318  ioof  10391  fzf  10433  fzp1disj  10505  fzp1nel  10529  fzo0  10595  frecfzennn  10885  frechashgf1o  10887  xnn0nnen  10896  fxnn0nninf  10898  seq3f1olemp  10974  sq0  11089  irec  11098  hash0  11258  prhash2ex  11273  hashfibclem  11305  hashf1lem1  11308  climmo  12090  sum0  12181  fisumcom2  12231  prod0  12378  fprodcom2fi  12419  cos1bnd  12552  cos2bnd  12553  3dvds  12657  n2dvdsm1  12706  n2dvds3  12708  flodddiv4  12729  3lcm2e6woprm  12890  6lcm4e12  12891  2prm  12931  3lcm2e6  12965  pockthi  13167  mod2xnegi  13228  modsubi  13229  ballotfilemcdc  13282  ballotfilem2  13287  ballotfilemic  13309  ballotfilem7  13338  ballotfilemth  13340  unennn  13347  ssnnctlemct  13396  structcnvcnv  13427  strleun  13518  starvndxnbasendx  13556  starvndxnplusgndx  13557  starvndxnmulrndx  13558  scandxnbasendx  13568  scandxnplusgndx  13569  scandxnmulrndx  13570  vscandxnbasendx  13573  vscandxnplusgndx  13574  vscandxnmulrndx  13575  vscandxnscandx  13576  ipndxnbasendx  13586  ipndxnplusgndx  13587  ipndxnmulrndx  13588  slotsdifipndx  13589  tsetndxnplusgndx  13606  tsetndxnmulrndx  13607  tsetndxnstarvndx  13608  slotstnscsi  13609  plendxnplusgndx  13620  plendxnmulrndx  13621  plendxnscandx  13622  plendxnvscandx  13623  slotsdifplendx  13624  basendxnocndx  13627  plendxnocndx  13628  dsndxnplusgndx  13635  dsndxnmulrndx  13636  slotsdnscsi  13637  dsndxntsetndx  13638  slotsdifdsndx  13639  unifndxntsetndx  13645  slotsdifunifndx  13646  restid  13664  mgmidmo  13752  gsum0cmn  14245  gsum2d2fi  14275  gsumcom2fi  14276  prdsval  14281  mgpplusg  14330  ringidval  14373  opprringb  14496  reldvdsr  14508  rrgmex  14679  lssmex  14802  lidlmex  14922  2idlmex  14948  asclfval  15131  fczpsrbag  15171  tgdom  15310  tgidm  15312  resttopon  15409  rest0  15417  psmetrel  15560  metrel  15580  xmetrel  15581  xmetf  15588  0met  15622  mopnrel  15679  setsmsbasg  15717  setsmsdsg  15718  qtopbasss  15759  reldvg  15917  dvexp  15949  dveflem  15964  elply2  15973  elplyd  15979  ply1term  15981  plymullem  15988  efcn  16006  sinhalfpilem  16030  sincosq1lem  16064  tangtx  16077  sincos4thpi  16079  pigt3  16083  dfrelog  16101  relogf1o  16102  log1  16107  loge  16108  relogiso  16115  2logb9irr  16219  2logb9irrap  16225  log2ublem1  16233  birthdaylog2  16240  ppiqltx  16293  ppiublem1  16303  ppiqub  16305  bclbnd  16319  bpos1lem  16321  bposlem8  16330  2sqlem9  16460  2sqlem10  16461  uhgr0e  16540  uhgr0  16543  umgrbien  16568  usgr0  16697  griedg0prc  16708  1loopgruspgr  16761  konigsbergumgr  16945  konigsberglem1  16946  ex-fl  16956  bj-nndcALT  17003  bj-axempty  17136  bj-axempty2  17137  bdinex1  17142  bj-zfpair2  17153  bj-uniex2  17159  bj-indint  17174  bj-omind  17177  bj-omex  17185  bj-omelon  17204  pw1ndom3  17237  wexmiddifxylem  17262  0nninf  17265  dceqnconst  17329  dcapnconst  17330