Theorem mpbir 190

Description: An inference from a biconditional, related to modus ponens.

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	biimpr 152	. 2 ⊢ (ψ → φ)
4	1, 3	ax-mp 7	1 ⊢ φ

Syntax hints:   ↔ wb 146

This theorem is referenced by:  mtbir 192  orri 231  imp 350  con4bii 521  pm3.2ni 578  pm5.74ri 585  pm3.24 656  pm5.16 665  mpbir2an 728  nicodmpraw 950  19.35ri 1073  ax9o 1118  a9e 1121  cbval2 1311  cbvex2 1312  moaneu 1423  moanmo 1424  axext 1453  eqeltr 1536  mprgbir 1693  visset 1804  issetri 1807  eueq3 1910  moeq 1911  ru 1928  eqsstr 2081  3sstr4 2090  ssnpss 2139  pwid 2398  pri1 2441  pwv 2492  uni0 2515  intab 2550  eqbrtr 2624  tr0 2681  trv 2682  zfrep4 2691  zfnuleu 2697  0ex 2701  inex1 2706  0elpw 2726  notzfaus 2731  pwex 2735  snex 2740  exss 2759  dvdemo1 2765  zfpair2 2770  moop2 2790  itlso 2854  uniex2 2860  rabxfr 2892  0elon 3012  nsuceq0 3043  limon 3084  onuninsuc 3098  finds 3146  finds2 3148  tfinds2 3155  onxpdisj 3231  relsn 3244  relxp 3245  relopab 3256  rel0 3262  reli 3263  rele 3264  ididg 3268  dmi 3315  relres 3371  relcnv 3419  relco 3470  cnvcnv 3472  isarep2 3564  opabex 3595  f0 3641  fconst 3643  f10 3698  f1o00 3699  f1oi 3702  f1osn 3704  fvopab3ig 3763  canth 3892  ncanth 3893  tfrlem8 3903  tz7.44lem1 3912  abianfp 3947  reloprab 3977  reldmoprab 3990  oprabex 4004  oprabex3 4007  oprabvalig 4009  oprabval3 4015  ndmoprcl 4030  fo1st 4075  fo2nd 4076  f1stres 4077  f2ndres 4078  df1st2 4110  df2nd2 4111  1ne0 4126  0lt1o 4131  th3qcor 4300  mapsspw 4325  map0 4328  relen 4354  reldom 4355  ssdomg 4389  ensn1 4405  limensuci 4486  omsdomnn 4509  unblem4 4520  prfi 4531  pm54.43 4546  inf2 4580  inf3lem6 4590  infeq5 4593  zfinf 4598  inf5 4600  trcl 4617  r1fnon 4622  r1tr 4626  tz9.12lem2 4632  tz9.12lem3 4633  jech9.3 4638  rankval 4640  rankr1 4646  rankpw 4656  karden 4698  aceq3lem 4704  ac2 4718  kmlem2 4738  numthlem 4755  numth2 4757  zorn 4769  cardon 4799  cardid 4800  sucxpdom 4818  ondomon 4828  cardprc 4833  alephfnon 4834  alephsucpw 4842  alephsucdom 4852  alephfplem4 4871  alephfp 4872  alephval3 4875  axpowndlem3 4923  zfcndun 4939  zfcndpow 4940  zfcndinf 4942  zfcndac 4943  dmaddpi 4990  dmmulpi 4991  1lt2pi 5004  1q 5029  1lt2pq 5050  1pr 5089  0r 5161  1r 5162  m1r 5163  m1p1sr 5173  m1m1sr 5174  0lt1sr 5176  axaddopr 5237  axmulopr 5238  ax1cn 5241  ax1ne0 5252  subaddri 5344  ine0 5406  pnfxr 5465  mnfxr 5466  pnfnre 5468  mnfnre 5469  pnfnemnf 5509  renfdisj 5512  mnfltpnf 5517  divrec 5700  div1 5728  recgt0i 5770  nn1suc 5887  4d2e2 5974  nnunb 6017  arch 6018  0z 6093  nneo 6144  om2uzran 6237  om2uzf1o 6238  uzrdgfnuz 6243  ndmioo 6307  ioof 6333  indstr 6393  elfzlem 6405  seq0fn 6478  dfseq0 6495  sq0 6566  sqrlem6 6608  sqrlem8 6610  sqrlem11 6613  sqr4 6647  sqr9 6648  sqr2irr 6659  irec 6661  nthruz 6677  cjmulrcl 6726  abs0 6814  abstri 6829  abslem2i 6845  bcpasc2 6905  climrel 6914  climuz0 7045  iserzshft 7080  climabslem 7084  climubi 7089  climsup 7091  caucvg 7099  isumshft2 7140  isumcmpi 7150  infcvgaux1 7154  fnsmnt 7161  negfcncf 7204  ivthlem5 7220  ivthlem6 7221  ivthlem7 7222  ivthlem8 7223  isupivth 7225  ivthlem5OLD 7229  ivthlem6OLD 7230  ivthlem7OLD 7231  ivthlem8OLD 7232  ivth2OLD 7234  efaddlem8 7287  efaddlem12 7291  ef1tllem 7323  eirrlem1 7330  eirrlem3 7332  eirr 7335  reeff1o 7368  sinadd 7393  cos2tOLD 7406  cos1bnd 7416  cos2bnd 7417  acdc2lem2 7431  acdc5lem2 7434  nnenom 7440  unbenlem 7447  ruclem13 7465  ruclem35 7487  aleph1re 7494  eltopsp 7546  tpsex 7547  subbas 7586  sn0top 7589  indistps 7595  distps 7596  retopbas 7597  msrel 7736  0met 7765  cnmet 7843  bcthlem12 7944  isgrpi 7976  0ngrp 7989  isgrp2i 8011  issubgi 8059  grpsn 8061  ablsn 8062  ghgrpilem4 8073  ghsubgi 8075  isring 8078  vcrel 8103  isvci 8139  nvrel 8159  0vfval 8163  isnvi 8171  isnviOLD 8172  vsfval 8194  ipcl 8299  ajmoi 8450  ajfuni 8451  minvecdist 8516  pilem2 8591  sincosq1lem 8620  sincos4thpi 8627  sincos6thpi 8628  cosh111lem1 8629  efifolem2 8638  circgrpOLD 8658  logrn 8673  eff1o2 8676  logf1o 8677  relogf1o 8679  log1 8688  loge 8689  pilog 8690  relogiso 8697  log1OLD 8707  logeOLD 8708  logisoOLD 8714  axgroth2 8717  axgroth3 8718  avril1 8723  2bornot2b 8724  normlem2 8898  norm3adif 8936  hhssnv 9054  projlem13 9114  projlem14 9115  pjpj0 9170  shscl 9196  shsumval2 9275  h1de2 9391  fh3 9483  fh4 9484  qlaxr3 9494  ho0f 9594  hoif 9597  hodid 9630  ho0sub 9638  hosd1 9665  adjmo 9675  nmopsetn0 9709  nmfnsetn0 9722  funadj 9730  funcnvadj 9734  adj1o 9735  nlelsh 9908  cnlnadjlem8 9922  nmoptri2 9946  bra11 9954  pjoc 10018  pjinvar 10029  cvnsymt 10127  ghomgrpilem2 10291  symggrpiOLD 10311  symgidiOLD 10312  symggrpi 10313  symgidi 10314  ompfl2OLD 10327  cmpfun 10363  hmeogrp 10425  efilcp 10445  efilcp2 10450  dtopcl 10459  1ded 10515  relded 10517  reldded 10518  relrded 10519  relcat 10538  reldcat 10539  relrcat 10540  hgrarel 10604

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7

This theorem depends on definitions:  df-bi 147

Copyright terms: Public domain