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  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  3744  rabrsndc  3778  tpid1  3822  tpid2  3824  tpid3  3827  pwv  3932  uni0  3960  eqbrtri  4149  tr0  4238  trv  4239  zfnuleu  4255  0ex  4258  inex1  4265  elpwi2  4292  0elpw  4299  axpow2  4311  axpow3  4312  vpwex  4314  zfpair2  4345  exss  4365  opwo0id  4387  moop2  4390  pwundifss  4428  po0  4454  epse  4485  fr0  4494  0elon  4535  onm  4544  uniex2  4579  uniex2OLD  4580  snnex  4592  ordtriexmidlem  4664  ordtriexmid  4666  ontr2exmid  4670  ordtri2or2exmidlem  4671  onsucsssucexmid  4672  onsucelsucexmidlem  4674  ruALT  4696  zfregfr  4719  dcextest  4726  zfinf2  4734  omex  4738  finds  4745  finds2  4746  ordom  4752  omsinds  4767  relsnop  4879  relxp  4882  rel0  4900  relopabiv  4901  relopabi  4903  eliunxp  4917  opeliunxp2  4918  dmi  4994  xpidtr  5176  cnvcnv  5238  dmsn0  5253  cnvsn0  5254  funmpt  5413  funmpt2  5414  funinsn  5428  isarep2  5466  f0  5581  f10  5672  f10d  5673  f1o00  5674  f1oi  5677  f1osn  5679  brprcneu  5686  fvopab3ig  5776  opabex  5935  eufnfv  5943  rinvf1o  6029  mpofun  6184  reldmmpo  6194  ovid  6199  ovidig  6200  ovidi  6201  ovig  6204  ovi3  6220  relmptopab  6285  oprabex  6355  oprabex3  6356  f1stres  6387  f2ndres  6388  opeliunxp2f  6503  tpos0  6539  issmo  6553  tfrlem6  6581  tfrlem8  6583  tfri1dALT  6616  tfrcl  6629  rdgfun  6638  frecfun  6660  frecfcllem  6669  0lt1o  6707  eqer  6833  ecopover  6901  ecopoverg  6904  th3qcor  6907  mapsnf1o3  6973  ssdomg  7059  ensn1  7077  xpcomf1o  7117  fiunsnnn  7179  finexdc  7201  elssdc  7203  exmidpw  7209  fissfi  7257  dcfi  7309  omct  7451  infnninf  7458  infnninfOLD  7459  pm54.43  7530  exmidonfinlem  7539  pw1on  7579  pw1dom2  7580  pw1ne1  7582  2oneel  7616  dmaddpi  7686  dmmulpi  7687  1lt2pi  7701  indpi  7703  1lt2nq  7767  genpelxp  7872  ltexprlempr  7969  recexprlempr  7993  cauappcvgprlemcl  8014  cauappcvgprlemladd  8019  caucvgprlemcl  8037  caucvgprprlemcl  8065  m1p1sr  8121  m1m1sr  8122  0lt1sr  8126  peano1nnnn  8213  ax1cn  8222  ax1re  8223  axaddf  8229  axmulf  8230  ax0lt1  8237  0lt1  8447  subaddrii  8609  ixi  8905  1ap0  8912  sup3exmid  9281  nn1suc  9306  neg1lt0  9395  4d2e2  9448  iap0  9511  un0mulcl  9580  pnf0xnn0  9620  3halfnz  9726  nummac  9804  uzf  9907  mnfltpnf  10170  ixxf  10283  ioof  10356  fzf  10398  fzp1disj  10470  fzp1nel  10494  fzo0  10560  frecfzennn  10846  frechashgf1o  10848  xnn0nnen  10857  fxnn0nninf  10859  seq3f1olemp  10935  sq0  11050  irec  11059  hash0  11218  prhash2ex  11233  hashfibclem  11265  hashf1lem1  11268  climmo  12047  sum0  12138  fisumcom2  12188  prod0  12335  fprodcom2fi  12376  cos1bnd  12509  cos2bnd  12510  3dvds  12614  n2dvdsm1  12663  n2dvds3  12665  flodddiv4  12686  3lcm2e6woprm  12847  6lcm4e12  12848  2prm  12888  3lcm2e6  12921  pockthi  13120  modsubi  13181  ballotfilemcdc  13206  ballotfilem2  13211  ballotfilemic  13233  ballotfilem7  13262  ballotfilemth  13264  unennn  13271  ssnnctlemct  13320  structcnvcnv  13351  strleun  13441  starvndxnbasendx  13479  starvndxnplusgndx  13480  starvndxnmulrndx  13481  scandxnbasendx  13491  scandxnplusgndx  13492  scandxnmulrndx  13493  vscandxnbasendx  13496  vscandxnplusgndx  13497  vscandxnmulrndx  13498  vscandxnscandx  13499  ipndxnbasendx  13509  ipndxnplusgndx  13510  ipndxnmulrndx  13511  slotsdifipndx  13512  tsetndxnplusgndx  13529  tsetndxnmulrndx  13530  tsetndxnstarvndx  13531  slotstnscsi  13532  plendxnplusgndx  13543  plendxnmulrndx  13544  plendxnscandx  13545  plendxnvscandx  13546  slotsdifplendx  13547  basendxnocndx  13550  plendxnocndx  13551  dsndxnplusgndx  13558  dsndxnmulrndx  13559  slotsdnscsi  13560  dsndxntsetndx  13561  slotsdifdsndx  13562  unifndxntsetndx  13568  slotsdifunifndx  13569  restid  13587  mgmidmo  13675  gsum0cmn  14137  prdsval  14156  mgpplusg  14205  ringidval  14248  opprringb  14369  reldvdsr  14381  rrgmex  14552  lssmex  14675  lidlmex  14795  2idlmex  14821  asclfval  15004  fczpsrbag  15039  tgdom  15156  tgidm  15158  resttopon  15255  rest0  15263  psmetrel  15406  metrel  15426  xmetrel  15427  xmetf  15434  0met  15468  mopnrel  15525  setsmsbasg  15563  setsmsdsg  15564  qtopbasss  15605  reldvg  15763  dvexp  15795  dveflem  15810  elply2  15819  elplyd  15825  ply1term  15827  plymullem  15834  efcn  15852  sinhalfpilem  15875  sincosq1lem  15909  tangtx  15922  sincos4thpi  15924  pigt3  15928  dfrelog  15944  relogf1o  15945  log1  15950  loge  15951  relogiso  15957  2logb9irr  16056  2logb9irrap  16062  log2ublem1  16066  birthdaylog2  16073  2sqlem9  16226  2sqlem10  16227  uhgr0e  16306  uhgr0  16309  umgrbien  16334  usgr0  16463  griedg0prc  16474  1loopgruspgr  16527  konigsbergumgr  16711  konigsberglem1  16712  ex-fl  16722  bj-nndcALT  16769  bj-axempty  16902  bj-axempty2  16903  bdinex1  16908  bj-zfpair2  16919  bj-uniex2  16925  bj-indint  16940  bj-omind  16943  bj-omex  16951  bj-omelon  16970  pw1ndom3  17003  0nninf  17021  dceqnconst  17084  dcapnconst  17085