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 522  pm3.2ni 579  pm5.74ri 586  pm3.24 657  pm5.16 666  mpbir2an 729  nicodmpraw 952  19.35ri 1076  ax9o 1121  a9e 1124  cbval2 1315  cbvex2 1316  moaneu 1429  moanmo 1430  axext 1459  eqeltr 1542  mprgbir 1699  visset 1810  issetri 1813  eueq3 1916  moeq 1917  ru 1935  eqsstr 2088  3sstr4 2097  ssnpss 2146  pwid 2405  pri1 2447  pwv 2498  uni0 2521  intab 2556  eqbrtr 2630  tr0 2687  trv 2688  zfrep4 2697  zfnuleu 2703  0ex 2707  inex1 2712  0elpw 2732  notzfaus 2737  pwex 2741  snex 2746  exss 2765  dvdemo1 2771  zfpair2 2776  moop2 2797  itlso 2859  uniex2 2865  rabxfr 2898  0elon 3018  nsuceq0 3049  limon 3090  onuninsuc 3104  finds 3152  finds2 3154  tfinds2 3161  onxpdisj 3237  relsn 3250  relxp 3251  relopab 3262  rel0 3268  reli 3269  rele 3270  ididg 3274  dmi 3322  relres 3383  relcnv 3431  relco 3480  cnvcnv 3482  isarep2 3574  opabex 3605  f0 3651  fconst 3653  f10 3708  f1o00 3709  f1oi 3712  f1osn 3714  fvopab3ig 3773  canth 3902  ncanth 3903  tfrlem8 3913  tz7.44lem1 3922  abianfp 3957  reloprab 3987  reldmoprab 4000  oprabex 4014  oprabex3 4017  oprabvalig 4019  oprabval3 4025  ndmoprcl 4039  fo1st 4084  fo2nd 4085  f1stres 4086  f2ndres 4087  df1st2 4119  df2nd2 4120  1ne0 4135  0lt1o 4140  th3qcor 4309  mapsspw 4334  map0 4337  relen 4363  reldom 4364  ssdomg 4398  ensn1 4414  limensuci 4495  omsdomnn 4518  unblem4 4529  prfi 4540  pm54.43 4555  inf2 4591  inf3lem6 4601  infeq5 4604  zfinf 4609  inf5 4611  trcl 4628  r1fnon 4633  r1tr 4637  tz9.12lem2 4643  tz9.12lem3 4644  jech9.3 4649  rankval 4651  rankr1 4657  rankpw 4667  karden 4709  aceq3lem 4715  ac2 4729  kmlem2 4749  numthlem 4766  numth2 4768  zorn 4780  cardon 4810  cardid 4811  sucxpdom 4829  ondomon 4839  cardprc 4844  alephfnon 4845  alephsucpw 4853  alephsucdom 4863  alephfplem4 4882  alephfp 4883  alephval3 4886  axpowndlem3 4934  zfcndun 4950  zfcndpow 4951  zfcndinf 4953  zfcndac 4954  dmaddpi 5001  dmmulpi 5002  1lt2pi 5015  1q 5040  1lt2pq 5061  1pr 5100  0r 5172  1r 5173  m1r 5174  m1p1sr 5184  m1m1sr 5185  0lt1sr 5187  axaddopr 5248  axmulopr 5249  ax1cn 5252  ax1ne0 5263  subaddri 5355  ine0 5417  pnfxr 5476  mnfxr 5477  pnfnre 5479  mnfnre 5480  pnfnemnf 5519  renfdisj 5522  mnfltpnf 5527  divrec 5710  div1 5738  recgt0i 5780  nn1suc 5897  4d2e2 5984  nnunb 6027  arch 6028  0z 6103  nneo 6154  om2uzran 6250  om2uzf1o 6251  uzrdgfnuz 6256  ndmioo 6320  ioof 6346  indstr 6406  elfzlem 6418  seq0fn 6491  dfseq0 6508  sq0 6580  sqrlem6 6623  sqrlem8 6625  sqrlem11 6628  sqr4 6662  sqr9 6663  sqr2irr 6674  irec 6676  nthruz 6692  cjmulrcl 6741  abs0 6829  abstri 6844  abslem2i 6860  bcpasc2 6920  climrel 6929  climuz0 7061  iserzshft 7097  climabslem 7101  climubi 7106  climsup 7108  caucvg 7116  isumshft2 7157  isumcmpi 7167  infcvgaux1 7171  fnsmnt 7178  negfcncf 7221  ivthlem5 7237  ivthlem6 7238  ivthlem7 7239  ivthlem8 7240  isupivth 7242  ivthlem5OLD 7246  ivthlem6OLD 7247  ivthlem7OLD 7248  ivthlem8OLD 7249  ivth2OLD 7251  efaddlem8 7304  efaddlem12 7308  ef1tllem 7340  eirrlem1 7347  eirrlem3 7349  eirr 7352  reeff1o 7385  sinadd 7410  cos2tOLD 7423  cos1bnd 7433  cos2bnd 7434  acdc2lem2 7448  acdc5lem2 7451  nnenom 7457  unbenlem 7464  ruclem13 7482  ruclem35 7504  aleph1re 7511  eltopsp 7564  tpsex 7565  subbas 7604  sn0top 7607  indistps 7613  distps 7614  retopbas 7615  msrel 7757  0met 7787  cnmet 7866  bcthlem12 7972  isgrpi 8004  0ngrp 8017  isgrp2i 8038  issubgi 8086  grpsn 8088  ablsn 8089  ghgrpilem4 8100  ghsubgi 8102  isring 8105  vcrel 8130  isvci 8165  nvrel 8185  0vfval 8189  isnvi 8196  vsfval 8218  ipcl 8327  ajmoi 8478  ajfuni 8479  minvecdist 8544  pilem2 8626  sincosq1lem 8655  sincos4thpi 8662  sincos6thpi 8663  cosh111lem1 8664  efifolem2 8673  circgrpOLD 8693  logrn 8706  eff1o2 8709  logf1o 8710  relogf1o 8712  log1 8721  loge 8722  pilog 8723  relogiso 8730  axgroth2 8733  axgroth3 8734  avril1 8739  2bornot2b 8740  normlem2 8932  norm3adif 8970  hhssnv 9089  projlem13 9153  projlem14 9154  pjpj0 9210  shscl 9236  shsumval2 9315  h1de2 9431  fh3 9523  fh4 9524  qlaxr3 9534  ho0f 9634  hoif 9637  hodid 9670  ho0sub 9678  hosd1 9705  adjmo 9715  nmopsetn0 9749  nmfnsetn0 9762  funadj 9770  funcnvadj 9774  adj1o 9775  nlelsh 9949  cnlnadjlem8 9963  nmoptri2 9988  bra11 9997  pjoc 10064  pjinvar 10075  cvnsymt 10173  ghomgrpilem2 10342  symggrpi 10362  symgidi 10363  cmpfun 10421  hmeogrp 10484  efilcp 10504  efilcp2 10509  dtopcl 10531  1ded 10587  relded 10589  reldded 10590  relrded 10591  relcat 10610  reldcat 10611  relrcat 10612  hgrarel 10677

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