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

Syntax hints:   ↔ wb 104

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 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  666  stabnot  784  mpbir2an  894  mpbir3an  1131  tru  1303  mpgbir  1397  nfxfr  1418  19.8a  1537  sbt  1725  dveeq2  1754  dveeq2or  1755  sbequilem  1777  cbvex2  1857  dvelimALT  1946  dvelimfv  1947  dvelimor  1954  nfeuv  1978  moaneu  2036  moanmo  2037  eqeltri  2172  nfcxfr  2237  neir  2270  neirr  2276  eqnetri  2290  nesymir  2314  nelir  2365  mprgbir  2449  vex  2644  issetri  2650  moeq  2812  cdeqi  2847  ru  2861  eqsstri  3079  3sstr4i  3088  rgenm  3412  mosn  3507  rabrsndc  3538  tpid1  3581  tpid2  3583  tpid3  3586  pwv  3682  uni0  3710  eqbrtri  3894  tr0  3977  trv  3978  zfnuleu  3992  0ex  3995  inex1  4002  0elpw  4028  axpow2  4040  axpow3  4041  vpwex  4043  zfpair2  4070  exss  4087  moop2  4111  pwundifss  4145  po0  4171  epse  4202  fr0  4211  0elon  4252  onm  4261  uniex2  4296  snnex  4307  ordtriexmidlem  4373  ordtriexmid  4375  ontr2exmid  4378  ordtri2or2exmidlem  4379  onsucsssucexmid  4380  onsucelsucexmidlem  4382  ruALT  4404  zfregfr  4426  dcextest  4433  zfinf2  4441  omex  4445  finds  4452  finds2  4453  ordom  4458  omsinds  4473  relsnop  4583  relxp  4586  rel0  4602  relopabi  4603  eliunxp  4616  opeliunxp2  4617  dmi  4692  xpidtr  4865  cnvcnv  4927  dmsn0  4942  cnvsn0  4943  funmpt  5097  funmpt2  5098  funinsn  5108  isarep2  5146  f0  5249  f10  5335  f1o00  5336  f1oi  5339  f1osn  5341  brprcneu  5346  fvopab3ig  5427  opabex  5576  eufnfv  5580  mpofun  5805  reldmmpo  5814  ovid  5819  ovidig  5820  ovidi  5821  ovig  5824  ovi3  5839  oprabex  5957  oprabex3  5958  f1stres  5988  f2ndres  5989  opeliunxp2f  6065  tpos0  6101  issmo  6115  tfrlem6  6143  tfrlem8  6145  tfri1dALT  6178  tfrcl  6191  rdgfun  6200  frecfun  6222  frecfcllem  6231  0lt1o  6267  eqer  6391  ecopover  6457  ecopoverg  6460  th3qcor  6463  mapsnf1o3  6521  ssdomg  6602  ensn1  6620  xpcomf1o  6648  fiunsnnn  6704  finexdc  6725  exmidpw  6731  infnninf  6934  nnnninf  6935  pm54.43  6957  dmaddpi  7034  dmmulpi  7035  1lt2pi  7049  indpi  7051  1lt2nq  7115  genpelxp  7220  ltexprlempr  7317  recexprlempr  7341  cauappcvgprlemcl  7362  cauappcvgprlemladd  7367  caucvgprlemcl  7385  caucvgprprlemcl  7413  m1p1sr  7456  m1m1sr  7457  0lt1sr  7461  peano1nnnn  7539  ax1cn  7548  ax1re  7549  ax0lt1  7561  0lt1  7760  subaddrii  7922  ixi  8211  1ap0  8218  sup3exmid  8573  nn1suc  8597  neg1lt0  8686  4d2e2  8732  iap0  8795  un0mulcl  8863  pnf0xnn0  8899  3halfnz  9000  nummac  9078  uzf  9179  mnfltpnf  9412  ixxf  9522  ioof  9595  fzf  9635  fzp1disj  9701  fzp1nel  9725  fzo0  9786  frecfzennn  10040  frechashgf1o  10042  fxnn0nninf  10052  seq3f1olemp  10116  sq0  10224  irec  10233  hash0  10384  prhash2ex  10396  climmo  10906  sum0  10996  fisumcom2  11046  cos1bnd  11264  cos2bnd  11265  n2dvdsm1  11405  n2dvds3  11407  flodddiv4  11426  3lcm2e6woprm  11560  6lcm4e12  11561  2prm  11601  3lcm2e6  11631  unennn  11702  structcnvcnv  11757  strleun  11830  restid  11913  tgdom  12023  tgidm  12025  resttopon  12122  rest0  12130  psmetrel  12250  metrel  12270  xmetrel  12271  xmetf  12278  0met  12312  mopnrel  12369  setsmsbasg  12407  setsmsdsg  12408  qtopbasss  12443  reldvg  12521  ex-fl  12540  bj-axempty  12672  bj-axempty2  12673  bdinex1  12678  bj-zfpair2  12689  bj-uniex2  12695  bj-indint  12714  bj-omind  12717  bj-omex  12725  bj-omelon  12744  pw1dom2  12775  0nninf  12781