Theorem mpbi 189

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

Hypotheses

Ref	Expression
mpbi.min	⊢ φ
mpbi.maj	⊢ (φ ↔ ψ)

Assertion

Ref	Expression
mpbi	⊢ ψ

Proof of Theorem mpbi

Step	Hyp	Ref	Expression
1		mpbi.min	. 2 ⊢ φ
2		mpbi.maj	. . 3 ⊢ (φ ↔ ψ)
3	2	biimp 151	. 2 ⊢ (φ → ψ)
4	1, 3	ax-mp 7	1 ⊢ ψ

Syntax hints:   ↔ wb 146

This theorem is referenced by:  mtbi 191  ori 230  ex 373  pm5.74i 586  pm4.71i 639  pm4.71ri 640  pm5.32i 647  pm5.16 669  pm5.19 671  pm5.55 677  biluk 747  3ori 887  nicodraw 954  19.35i 1078  19.36i 1081  exan 1108  sbco 1254  19.37aiv 1306  equsb3lem 1331  elsb3 1333  eqcomi 1482  eqtr 1498  eleqtr 1549  nemtbir 1644  nrex 1732  isseti 1818  vtocl2 1846  vtocl3 1847  eueq1 1920  euxfr2 1929  csbief 2035  ssid 2083  sseqtr 2096  3sstr3 2102  unssi 2208  ssini 2236  unabs 2241  inabs 2242  dfin4 2251  noel 2287  rab0 2297  difid 2338  difdisj 2341  ifor 2385  snid 2439  snsssn 2482  intab 2564  breqtr 2643  axrep1 2699  axsep 2707  bm1.3ii 2711  zfnuleu 2712  0nep0 2742  notzfaus 2746  axpow 2749  dtruALT 2754  dtru 2778  opprc1b 2802  uniop 2814  axun 2873  rabxfr 2908  reuxfr2 2909  op1stb 2919  fr0 2933  onunisuc 3112  omon 3149  relop 3281  dmsnsn0 3331  rn0 3361  dmresi 3405  cnvcnv 3492  cnvcnvres 3500  cocnvcnv2 3512  cores2 3513  co01 3515  isarep2 3584  fnopab 3623  f1cnv 3672  f1ovi 3724  fvprc 3727  fvopabn 3792  fvsnun2 3802  fopab 3833  xpsn 3841  fvi 3848  tfrlem13 3929  tz7.44-2 3935  tz7.44-3 3936  frfnom 3957  oprabss 4012  2nd0 4090  f1stres 4099  f2ndres 4100  foprab 4126  fnoprab2 4128  2on 4145  xp01disj 4149  oawordeulem 4194  oarec 4202  ersym 4278  ertr 4280  0nelqs 4304  dfdom2 4390  dmen 4413  ssdomg 4414  2dom 4433  sbthlem5 4457  mapdom2lem 4499  limensuci 4512  fiint 4572  fiintOLD 4573  pwfilem 4577  pwfilemOLD 4578  suc11reg 4614  axinf 4632  axinf2 4633  tz9.13 4673  rankval 4678  ssrankr1 4686  rankpw 4694  rankop 4703  rankeq0 4706  ranksuc 4710  rankelun 4717  rankxplim 4722  rankxplim3 4724  rankxpsuc 4725  cp 4732  bnd 4733  karden 4736  axac 4755  ac3 4757  ac5 4762  ac6lem 4764  brdom3 4811  card0 4833  cardom 4835  cardval 4836  card1 4843  cardlim 4862  alephsuc 4877  aleph1 4882  alephgeom 4893  unialeph 4906  cffnon 4919  cf0 4922  cfsuc 4927  pm110.643 4935  cdaassen 4942  zfcndrep 4978  zfcndpow 4980  zfcndac 4983  dmaddpi 5030  dmmulpi 5031  1lt2pi 5044  dmrecpq 5086  1lt2pq 5090  renegcl 5428  ine0 5446  ltxrltt 5512  renepnft 5549  renemnft 5550  renfdisj 5551  xrltnrt 5553  pnfnltt 5558  nltmnft 5559  mulnzcnopr 5714  divcan2 5728  eqneg 5806  negn0 5810  recgt0i 5816  posex 5910  nnsub 5958  halflt1 6032  lbinfm 6050  infmsup 6070  infmxrcl 6088  nn0mulcl 6124  nn0ltp1let 6129  nn0ssz 6154  elnnz1 6157  zltp1let 6183  nneo 6199  zeot 6201  uzrdgfnuz 6307  ser1cl2 6334  iccf 6402  dfioo2 6404  uzinfm 6463  limsupvalt 6530  sumsqne0 6635  nnlesq 6662  nnesq 6663  sqrlem1 6674  sqrlem2 6675  sqrlem10 6683  sqrlem11 6684  sqrlem15 6688  sqrlem16 6689  sqrlem19 6692  sqrlem20 6693  sqrmuli 6705  sqr2gt1lt2 6720  sqr2irrlem1 6725  inelr 6736  nthruc 6746  ipcn 6790  cjmulval 6792  re0 6820  im0 6821  re1 6822  im1 6823  cj0 6826  absid 6861  absi 6878  abstri 6891  abslem2i 6908  faclbnd4lem1 6948  bcpasc2 6967  bcpasc 6969  ser0mulc 7059  ser1mulc 7060  climunii 7098  climabslem 7148  climsup 7155  caucvg 7163  cvgcmpub 7185  isumcmpi 7215  isumsplit 7216  isum0split 7217  infcvglem1 7221  fnsmntlem 7225  fnsmnt 7226  expcnvlem1 7227  expcnvlem2 7228  expcnvlem4 7230  geolimilem 7235  geolim1i 7238  0.999... 7246  negfcncf 7269  ivthlem6 7286  ivthlem7 7287  ivthlem8 7288  dsupivthlem 7291  efcltlem1 7304  dfef2 7307  reefcl 7317  ele3lem 7326  ege2lem2 7328  ege2le3lem2 7329  efaddlem7 7344  efaddlem8 7345  efaddlem10 7347  efaddlem12 7349  efaddlem20 7357  efaddlem22 7359  efne0t 7369  eftlexOLD 7377  ef1tllem 7381  ef01tllem1 7383  ef01tllem2 7384  ef01tllem2OLD 7385  absef01tllem 7387  eirrlem1 7389  eirrlem3 7391  eirrlem4 7392  efsep 7396  effsumle 7397  efgt0 7404  efm1lim 7411  eflegeolem2 7414  efm1legeo 7417  efcnlem1 7419  efcnlem2 7420  reeff1o 7426  reeff1o2 7427  sin0ALT 7445  sin01bndlem1 7468  cos01bndlem2 7471  cos2bnd 7476  sin01gt0 7477  cos01gt0 7478  sincos2sgn 7481  sin4lt0 7482  acdc2lem2 7490  acdc5lem2 7493  ruclem6 7516  ruclem8 7518  ruclem17 7527  ruclem25 7535  ruclem26 7536  ruclem27 7537  infdif 7569  remetba 7906  dscmet 7915  xplm 7972  bcthlem33 8028  bcth 8029  isgrp2i 8072  cnid 8123  mulid 8128  ghgrpilem1 8129  ghgrpilem2 8130  ghgrpilem3 8131  ghgrpilem4 8132  ghsubgi 8134  vcoprnelem 8193  vcoprne 8194  vcex 8195  cnnvm 8309  ip1cnilem2 8370  ip1cnilem6 8374  ipasslem6 8491  ipasslem8 8493  ipasslem10 8495  minveclem14 8554  sincolem 8660  pilem1 8666  pilem2 8667  pilem3 8668  pigt2lt4 8670  sinhalfpilem 8674  sincos4thpi 8705  sincos6thpi 8706  cosh111lem1 8709  cosh111t 8712  efghgrpilem 8714  efifolem1 8717  efifolem2 8718  efifolem3 8719  efifolem4 8720  efifolem6 8722  efif1lem5 8729  efif1lem6 8730  efif1lem7 8731  logrn 8746  resslogrn 8748  dfrelog 8751  pilog 8763  logltbt 8771  axgroth4 8775  grothprim 8778  avril1 8779  normlem1 8971  normlem6 8976  normlem7 8977  norm-ii 8999  norm3adif 9010  hilid 9023  hilnorm 9025  hlimunii 9103  norm1ex 9117  hhssabl 9127  hhssnv 9129  hhshsslem1 9132  projlem3 9183  projlem5 9185  projlem12 9192  projlem14 9194  projlem15 9195  projlem18 9198  projlemHIL 9213  shincl 9326  shsumval2 9355  shs0 9367  chj0 9373  chincl 9378  chdmm1 9395  shjshs 9410  chsup0 9466  spansnpj 9496  cmcmlem 9529  cmcmi 9535  cmcm2i 9536  cmcm3i 9537  pjidm 9612  pjssm 9621  pj0 9633  pjocin 9638  pjrn 9642  df0op2 9673  hoaddcom 9693  hoaddass 9697  hocadddir 9700  hocsubdir 9701  hoaddid1 9707  ho0co 9709  hoid1 9710  hoid1r 9711  hodseq 9715  honegsub 9717  adj1o 9813  hoddi 9909  lnopunilem1 9930  lnopunilem2 9931  nmcopexlem2 9947  nmcopext 9954  nmcoplbt 9955  nmcfnexlem2 9976  nmcfnext 9983  nmcfnlbt 9984  adjbd1o 10013  adjco 10028  nmopcoadj 10029  pjsdi 10078  pjddi 10079  pjidmco 10100  pjtot 10102  pjin1 10115  pjclem1 10118  stji1 10164  large 10189  ghomgrpilem1 10380  ghomgrpilem2 10381  cayleylem2 10405  cayleylem3 10406  ump 10449  cmpfun 10457  vxveqv 10467  top2usne 10535  fgsb 10555  fgsb2 10560  cnfilca 10562  rcfpfillem5 10567  clicls 10593  stoi 10610  relrded 10646  relrcat 10667

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