Theorem mpbir 165

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

Syntax hints:   ↔ wb 127

This theorem is referenced by:  mtbir 167  orri 201  bicon4i 401  pm3.2ni 440  pm5.74ri 445  pm3.24 496  3pm3.2i 603  19.35ri 756  ax9 807  a9e 809  cbval2 974  cbvex2 975  axext 1086  eqeltr 1159  mprgbir 1250  visset 1350  issetri 1353  eueq3 1430  moeq 1431  ru 1437  sbc2or 1454  zfrep4 1479  eqssi 1517  eqsstr 1530  3sstr3 1538  ssnpss 1573  inex1 1697  pwid 1805  pwex 1806  pri1 1841  exss 1881  pwv 1884  moop2 1910  uniex 1947  tr0 2052  trv 2053  eqbrtr 2076  itlso 2151  we0 2196  ordon 2238  ord0 2276  0elon 2277  limon 2342  onuninsuc 2356  finds 2397  finds2 2399  tfinds2 2405  onxpdisj 2476  relsn 2485  relxp 2486  relopab 2494  rel0 2499  reli 2500  rele 2501  dmi 2545  relres 2591  relcnv 2624  cnvun 2642  relco 2658  cnvcnv 2661  funsn 2690  funi 2692  fnresi 2737  fn0 2739  funopabex 2742  f0 2772  fconst 2774  f10 2822  f1o00 2823  f1o0 2824  f1oi 2825  f1osn 2827  fvopab3ig 2869  fvi 2900  isoid 2933  canth 2945  ncanth 2946  tfrlem7 2955  tfr1 2962  tz7.44lem1 2965  tz7.44-1 2966  tz7.44-2 2967  frfnom 2989  abianfp 3000  reloprab 3022  reldmoprab 3034  funoprab 3037  fnoprab 3038  fnoprab2 3039  oprabex 3044  oprabex3 3046  oprabvalig 3048  oprabval3 3052  ndmoprcl 3058  fo1st 3094  fo2nd 3095  f1stres 3096  df1st2 3098  0lt1o 3116  oawordeulem 3156  th3qcor 3252  relen 3277  reldom 3278  ssdomg 3311  ensn1 3329  canth2 3381  xpmapenlem5 3395  limensuci 3401  omsdomnn 3424  unblem4 3434  unfilem2 3439  prfi 3444  inf0 3457  inf2 3459  inf3lem6 3469  inf5 3472  zfinf 3474  trcl 3489  r1fnon 3494  r1tr 3498  tz9.12lem2 3504  tz9.12lem3 3505  jech9.3 3510  rankval 3512  rankr1 3518  rankpw 3528  rankuni 3533  karden 3551  aceq3lem 3555  ac2 3567  kmlem2 3581  numthlem 3598  numth2 3600  zorn2 3612  cardon 3634  cardid 3635  sucxpdom 3652  ondomon 3662  cardprc 3667  alephfnon 3668  aleph1 3676  alephsucdom 3685  alephiso 3697  cfsuc 3709  axpowndlem3 3745  zfcndrep 3760  zfcndun 3761  zfcndpow 3762  zfcndinf 3764  zfcndac 3765  1pi 3805  dmaddpi 3812  dmmulpi 3813  1lt2pi 3826  1q 3851  1lt2pq 3872  1pr 3911  0r 3983  1r 3984  m1r 3985  m1p1sr 3995  m1m1sr 3996  0lt1sr 3998  ax0re 4063  ax1re 4064  axicn 4065  ax1ne0 4075  axi2m1 4082  negeu 4124  subneg 4148  subid1 4156  subdi 4182  receu 4215  divval 4217  divrec 4236  div1 4257  recgt0i 4385  nnind 4434  nn1suc 4435  4d2e2 4507  nnunb 4520  arch 4521  irec 4526  0nn0 4546  nn0ge0i 4559  0z 4573  indstr 4611  om2uzuz 4653  om2uzran 4655  om2uzf1o 4656  uzrdgini 4658  nneo 4719  sqrlem6 4736  sqrlem8 4738  sqrlem11 4741  sqrlem23 4753  sqr4 4772  sqr9 4773  sqr2irr 4782  nthruz 4785  reim0 4809  cjre 4811  cjmulrcl 4821  releabs 4858  abstri 4859  abslem2i 4866  facnnt 4870  fac0 4871  clim0 4882  ruclem13 4897  ruclem34 4918  ruclem35 4919  ruc 4924  nnenom 4926  qnnen 4931  normlem2 5064  norm3adif 5095  normpar2 5100  bcs 5101  hlim0 5140  hlimcaui 5141  helch 5151  hsn0elch 5155  occl 5188  projlem8 5200  projlem13 5205  projlem14 5206  pjpj0 5259  shscl 5282  shintcl 5294  chintcl 5296  shsumval2 5361  h1de2 5458  cmle 5511  qlaxr3 5529  osumlem7 5536  pjf 5588  ho0 5612  hodid 5616  hods0 5620  hosd1 5623  pjoc 5645  pjnel 5665  cvnsymt 5722

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

This theorem depends on definitions:  df-bi 128

metamath.org