Theorem mpbir 207

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

Hypotheses

Ref	Expression
mpbir.min	|- ps
mpbir.maj	|- (ph <-> ps)

Assertion

Ref	Expression
mpbir	|- ph

Proof of Theorem mpbir

Step	Hyp	Ref	Expression
1		mpbir.min	. 2 |- ps
2		mpbir.maj	. . 3 |- (ph <-> ps)
3	2	biimpri 169	. 2 |- (ps -> ph)
4	1, 3	ax-mp 7	1 |- ph

Syntax hints:   <-> wb 163

This theorem is referenced by:  mtbir 209  orri 248  imorri 253  imp 377  con4bii 582  pm3.2ni 640  pm5.74ri 647  pm3.24 720  pm5.16 730  mpbir2an 800  mpbir3an 1052  nic-mpALT 1238  nic-ax 1239  nic-axALT 1240  tru 1264  mpgbir 1334  19.35ri 1428  ax9o 1480  a9e 1483  sbt 1559  cbval2 1698  cbvex2 1699  moaneu 1830  moanmo 1831  euequ1 1861  axext2 1866  eqeltri 1967  exmidne 2022  mprgbir 2163  visset 2295  issetri 2298  eueq3 2430  moeq 2431  ru 2451  eqsstri 2647  3sstr4i 2656  ssnpssOLD 2713  pwid 3042  tpid1 3111  tpid2 3113  tpid3 3116  snsspr1 3135  pwv 3176  uni0 3205  unissintOLD 3242  intab 3247  eqbrtri 3356  tr0 3423  trv 3424  zfrep4 3436  zfnuleu 3442  0ex 3446  0exOLD 3447  inex1 3452  0elpw 3473  notzfaus 3478  axpow2 3483  axpow3 3484  pwex 3487  pwexOLD 3488  snexOLD 3493  exss 3516  dvdemo1 3520  zfpair2 3525  moop2 3548  po0 3601  itlso 3619  0elon 3716  sucidOLDOLD 3746  nsuceq0 3749  uniex2 3793  snnex 3801  onuninsuci 3921  tfinds2 3947  finds 3979  finds2 3981  onxpdisjOLD 4069  eqrelriv 4080  relsn 4087  relxp 4088  rel0 4102  relopab 4104  reli 4105  rele 4106  ididgOLD 4118  dmi 4172  dmiOLD 4173  relresOLD 4243  relcnv 4301  cotr 4302  cnvcnv 4359  dmsn0 4365  relco 4392  funsn 4463  isarep2 4499  opabex 4538  f0 4600  fconstOLD 4603  f10 4667  f1o00 4668  f1oi 4671  f1oiOLD 4672  f1osn 4674  f1osnOLD 4675  fvopab3ig 4741  eufnfv 4771  fopabsnOLD 4816  reloprab 4918  reldmoprab 4934  oprabex 4948  oprabex3 4951  oprabvalig 4953  oprabval3 4959  ndmoprcl 4977  fo1st 5032  fo2nd 5033  f1stres 5034  f2ndres 5035  fparlem3 5083  fparlem4 5084  canth 5112  ncanth 5113  tfrlem8 5126  tz7.44lem1 5135  abianfp 5171  1n0 5187  0lt1o 5192  ider 5326  th3qcor 5375  mapsspw 5400  map0 5403  relen 5431  reldom 5432  ssdomg 5467  ensn1 5483  snfi 5491  undefnel 5559  limensuci 5600  omsdomnn 5623  unblem4 5636  pm54.43 5662  hartog 5693  ruv 5704  ruALT 5705  inf2 5714  inf3lem6 5724  infeq5 5727  zfinf2 5732  inf5 5735  trcl 5752  r1fnon 5761  r1tr 5765  tz9.12lem2 5771  tz9.12lem3 5772  jech9.3 5777  rankval 5779  rankr1 5785  rankpw 5795  karden 5856  alephfnon 5873  omsublim 5887  aceq3lem 5894  ac2 5908  kmlem2 5928  numthlem 5945  numth2 5947  zorn 5959  cardon 5976  cardid 5977  sucxpdom 5998  ondomon 6008  cardprc 6013  alephsucpw 6018  alephsucdom 6028  alephfplem4 6047  alephfp 6048  alephval3 6051  nnacda 6088  axpowndlem3 6103  zfcndun 6119  zfcndpow 6120  zfcndinf 6122  zfcndac 6123  dmaddpi 6170  dmmulpi 6171  1lt2pi 6184  1q 6209  1lt2pq 6230  1pr 6269  0r 6341  1r 6342  m1r 6343  m1p1sr 6353  m1m1sr 6354  0lt1sr 6356  axaddopr 6417  axmulopr 6418  ax1cn 6422  ax1ne0 6433  subaddrii 6529  ine0 6597  pnfxrOLD 6661  pnfnre 6665  mnfnre 6666  pnfnemnf 6707  renfdisjOLD 6713  mnfltpnf 6719  ixi 6872  divreci 6920  div1i 6948  recgt0ii 6992  nn1suc 7122  4d2e2 7211  nnunb 7279  arch 7280  0z 7355  nneoi 7409  zindd 7427  ndmioo 7537  ioof 7569  indstr 7630  elfzlem 7643  om2uzrani 7711  om2uzf1oi 7712  uzrdgfnuzi 7718  seq1res 7740  seq1shftid 7769  seq1seqz 7784  seq1seq0 7788  seq0fn 7789  dfseq0 7806  sq0 7880  sqrlem6 7928  sqrlem8 7930  sqrlem11 7933  sqr4 7967  sqr9 7968  sqr2irr 7979  irec 7981  nthruz 7996  cjmulrcli 8041  abs0 8129  abstrii 8143  abslem2i 8160  bcpasc2i 8219  hashgf1o 8228  climrel 8236  climuz0i 8368  iserzshfti 8404  climabslem 8408  climubii 8413  climsupi 8415  caucvgi 8423  isumshft2i 8466  isumcmpii 8476  infcvgaux1i 8480  arisumi 8487  negfcncfi 8531  ivthlem6 8548  ivthlem7 8549  ivthlem8 8550  isupivthi 8552  efaddlem8 8607  efaddlem12 8611  ef1tllem 8643  ef01tllem1 8645  ef01tllem2 8646  eirrlem1 8651  eirrlem3 8653  eirr 8656  egt2OLD 8657  elt3OLD 8658  egt2lt3 8659  reeff1o 8691  sinaddi 8716  cos2OLD 8730  cos1bnd 8740  cos2bnd 8741  acdc2lem2 8758  acdc5lem2 8761  nnenom 8767  unbenlem 8773  ruclem13 8791  ruclem35 8813  aleph1re 8820  eltopsp 8873  tpsex 8874  subbas 8914  sn0top 8917  indistps 8923  distps 8924  retopbas 8925  msrel 9074  0met 9102  cnmet 9182  bcthlem12 9288  0ngrp 9335  fungid 9339  grpsn 9340  grpidval 9342  issubgi 9431  ghgrpilem4 9444  ghsubgi 9446  isgalem 9449  isring 9465  drngi 9493  vcrel 9498  nvrel 9553  0vfval 9557  vsfval 9586  vacnlem6 9672  ipcl 9704  ajmoi 9860  ajfuni 9861  minvecdist 9930  sinco 10016  cosco 10017  sincosq1lem 10052  sincos4thpi 10060  sincos6thpi 10061  cosh111lem1 10068  efifolem2 10077  logrn 10105  eff1o2 10108  logf1o 10109  relogf1o 10111  log1 10120  loge 10121  pilog 10122  relogiso 10129  axgroth5 10132  axgroth2 10133  grothpw 10134  axgroth6 10137  axgroth3 10138  avril1 10142  2bornot2b 10143  symggrpi 10205  symgidi 10206  relrng 10399  isdivrng 10417  normlem2 10610  norm3adifii 10648  hhssnv 10767  projlem13 10831  projlem14 10832  pjpj0i 10888  shscli 10914  shsumval2i 10993  h1de2i 11109  fh3i 11199  fh4i 11200  cm2mi 11202  qlaxr3i 11212  mayetes3i 11310  ho0f 11314  hoif 11317  hodidi 11350  ho0subi 11358  hosd1i 11385  adjmo 11395  nmopsetn0 11429  nmfnsetn0 11442  funadj 11450  funcnvadj 11454  lnopco0i 11566  nlelshi 11630  cnlnadjlem8 11644  nmoptri2i 11669  opsqrlem3 11713  hmopidmpji 11724  pjoci 11752  pjinvari 11764  cvnsym 11862  bnj52 12427  bnj100 12449  bnj99 12450  bnj224 12513  bnj585 12551  bnj597 12558  bnj855 12788  bnj859 12792  bnj870 12798  bnj992 12869  bnj993 12870  bnj994 12871  bnj995 12872  bnj1048 12888  bnj1059 12896  bnj1091 12912  bnj1101 12918  bnj1162 12954  bnj1305 13048  bnj1474 13151  bnj61 13204  bnj109 13226  bnj128 13238  bnj129 13239  bnj149 13241  bnj150 13242  bnj151 13243  bnj580 13301  bnj900 13325  bnj1008 13373  bnj1171 13439  ghomgrpilem2 13629  dvdslelem 13692  divalglem2 13698  divalglem5 13700  algrf 13739  eucalg 13755  mulgcdlem2 13757  1nprm 13769  isprm3 13776  2prm 13779  3prm 13780  4nprm 13781  mpt2fun 13843  domep 13861  2on0 13862  axextndbi 13871  predss 13885  poxp 13949  poseq 13954  wfrlem14 13970  wfrlem16 13972  sltval2 13997  nosgnn0i 14000  brv 14063  txprel 14066  relsset 14068  relbigcup 14073  fnbigcup 14075  fvbigcup 14076  waj-ax 14238  lukshef-ax2 14239  arg-ax 14240  trtrst 14330  unttr 14331  vxveqv 14357  cpref 14379  sqpeq 14383  prj1 14395  cmpfun 14480  inposet 14620  dominc 14622  rninc 14623  seqzp2 14716  symgfo 14730  zintdom 14787  vrrel 14833  hmeogrp 14892  efilcp 14922  efilcp2 14926  dtopcl 14948  singempcon 14965  istopgrp 14971  invtrgrp 14979  cntrsetlem 14999  leqrl 15022  lteqtpos 15024  miminf 15028  1ded 15085  relded 15087  reldded 15088  relrded 15089  relcat 15108  reldcat 15109  relrcat 15110  dualcat2 15133  settrcon 15247  tarval2 15249  tmpts 15257  hartogOLD 15384  omsublimOLD 15396  alexsublem4 15440  alexsub 15441  retopcon 15452  fnerel 15479  refrel 15487  fneerdm 15498  islocfin 15506  locfincomp 15514  neibastop2lem1 15519  neibastop2lem3 15521  neibastop2lem4 15522  fnejoin1 15530  fcluscomp 15621  filnet 15645  cover2 15673  prfunOLD 15677  brabg2 15681  abrexdom 15739  fdc 15812  csbrni 15832  trirni 15833  oprpiece1res1 15880  oprpiece1res2 15881  cnresoprab 15915  txmet 15925  totbndss 15937  heiborlem7 15961  heiborlem14 15968  heiborlem16 15970  heiborlem18 15972  heiborlem30 15984  heiborlem31 15985  heiborlem32 15986  bfplem1 15998  recms 16010  rrndm 16015  reparphtlem2 16064  pcoass 16085  isdivrng1 16109  hgrarel 16290  rusbcALT 16410  compne 16417  ipo0 16426  ifr0 16427  issmo 16443  dfvd1ir 16483  dfvd2ir 16492  dfvd3ir 16497  e0bir 16639  stb2xpl 16742  stb3xpl 16743  pleval2 16785  padd01 17272  padd02 17273

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 164

Copyright terms: Public domain