Theorem mpbir 209

Description: An inference from a biconditional, related to modus ponens. (Contributed by NM, 28-Dec-1992.)

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 206	. 2 |- ( ps -> ph )
4	1, 3	ax-mp 5	1 |- ph

Syntax hints:   <-> wb 184

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

This theorem depends on definitions:  df-bi 185

This theorem is referenced by:  pm5.74ri  246  con4bii  297  orri  376  imorri  414  imnani  423  mpbir2an  911  mpbir3an  1170  xorexmid  1366  tru  1373  nic-mpALT  1479  nic-ax  1480  nic-axALT  1481  mpgbir  1595  nfxfr  1615  19.35ri  1657  ax6ev  1710  exan  1900  cbvex2OLD  1977  ax13  1995  euequ1  2258  moanmo  2333  moaneuOLD  2335  axi12  2417  axext2  2420  eqeltri  2508  nfcxfr  2571  neir  2606  neirr  2608  exmidne  2609  eqnetri  2620  nesymir  2644  nelir  2703  mprgbir  2781  vex  2970  issetri  2974  moeq  3130  cdeqi  3166  eqsstri  3381  3sstr4i  3390  rabrsn  3940  tpid1  3983  tpid2  3984  tpid3  3986  pwv  4085  uni0  4113  eqbrtri  4306  tr0  4391  trv  4392  zfrep4  4406  zfnuleu  4413  axnulALT  4414  0ex  4417  inex1  4428  0elpw  4456  axpow2  4467  axpow3  4468  pwex  4470  dvdemo1  4522  zfpair2  4527  exss  4550  moop2  4581  pwundif  4623  po0  4651  epse  4698  0elon  4767  relsnop  4939  relxp  4942  rel0  4959  relopabi  4960  eliunxp  4972  opeliunxp2  4973  dmi  5049  xpidtr  5215  xpima  5275  cnvcnv  5285  dmsn0  5301  cnvsn0  5302  funmpt  5449  funmpt2  5450  isarep2  5493  fresaunres2  5578  f0  5587  f10  5667  f1o00  5668  f1oi  5671  f1osn  5673  brprcneu  5679  opabiotafun  5747  fvopab3ig  5766  opabex  5941  eufnfv  5946  canth  6044  ncanth  6045  mpt2fun  6187  reldmmpt2  6196  ovid  6202  ovidig  6203  ovidi  6204  ovig  6207  ov3  6222  caovmo  6295  relmptopab  6303  porpss  6359  uniex2  6370  snnex  6377  tfinds2  6469  finds  6497  finds2  6499  oprabex  6560  oprabex3  6561  f1stres  6593  f2ndres  6594  relmpt2opab  6650  tpos0  6770  issmo  6801  tfrlem6  6833  tfrlem8  6835  tfrlem16  6844  tfr1a  6845  tfr1  6848  tz7.44lem1  6853  seqomlem2  6898  seqomlem3  6899  seqomlem4  6900  fnseqom  6902  0lt1o  6936  0we1  6938  eqer  7126  ecopover  7196  th3qcor  7200  mapsnf1o3  7253  ssdomg  7347  ensn1  7365  snfi  7382  xpcomf1o  7392  map2xp  7473  limensuci  7479  sdom1  7504  unblem4  7559  fidomdm  7585  marypha1lem  7675  hartogslem1  7748  hartogs  7750  card2on  7761  ruALT  7809  inf2  7821  inf3lem6  7831  infeq5i  7834  zfinf2  7840  cantnflt  7872  cantnfltOLD  7902  cantnfOLD  7915  mapfienOLD  7919  cnfcom  7925  cnfcomOLD  7933  trcl  7940  tz9.1c  7942  tc2  7954  r1funlim  7965  r1fnon  7966  karden  8094  tskwe  8112  cardprclem  8141  pm54.43  8162  r0weon  8171  iunmapdisj  8185  alephfnon  8227  alephfplem4  8269  alephfp  8270  alephval3  8272  aceq3lem  8282  kmlem2  8312  cda1dif  8337  ackbij1  8399  ackbij2lem2  8401  ackbij2  8404  infpssrlem3  8466  hsmexlem4  8590  hsmexlem5  8591  axdc3lem4  8614  ac2  8622  axac3  8625  ac6  8641  axdclem2  8681  ondomon  8719  alephsucpw  8726  pwcfsdom  8739  cfpwsdom  8740  smobeth  8742  axpowndlem3  8756  axpowndlem3OLD  8757  zfcndun  8774  zfcndpow  8775  zfcndinf  8777  zfcndac  8778  wunex2  8897  uniwun  8899  wuncval2  8906  grur1  8979  axgroth5  8983  axgroth2  8984  axgroth6  8987  axgroth3  8990  grothtsk  8994  inaprc  8995  ltsopi  9049  dmaddpi  9051  dmmulpi  9052  1lt2pi  9066  nqerf  9091  addnqf  9109  mulnqf  9110  1lt2nq  9134  m1p1sr  9251  m1m1sr  9252  0lt1sr  9254  axaddf  9304  axmulf  9305  ax1cn  9308  subaddrii  9689  ixi  9957  recgt0ii  10230  nn1suc  10335  neg1lt0  10420  4d2e2  10470  arch  10568  un0mulcl  10606  nummac  10779  uzf  10856  indstr  10915  mnfltpnf  11098  ixxf  11302  ioof  11379  fzf  11433  fzp1disj  11507  fzof  11542  om2uzrani  11767  om2uzf1oi  11768  uzrdglem  11772  uzrdgfni  11773  uzrdg0i  11774  ltwenn  11777  hashgf1o  11785  axdc4uzlem  11796  sq0  11949  irec  11957  hashkf  12097  hashf  12102  hash0  12127  hashsslei  12168  hashxplem  12187  hashbclem  12197  hashf1lem1  12200  wrdexg  12236  wrd0  12244  revs1  12397  0csh0  12422  cshw1  12448  cats1fvn  12477  climmo  13027  fsumcom2  13233  ackbijnn  13283  incexclem  13291  infcvgaux1i  13311  efcvgfsum  13363  cos1bnd  13463  cos2bnd  13464  znnen  13487  qnnen  13488  aleph1re  13519  dvdslelem  13569  3dvds  13588  divalglem5  13593  bitsf  13615  sadcaddlem  13645  sadadd2lem  13647  sadadd3  13649  sadaddlem  13654  isprm3  13764  2prm  13771  phicl2  13835  pockthi  13960  unbenlem  13961  prmrec  13975  vdwlem13  14046  vdwnn  14051  ramcl2  14069  mod2xnegi  14092  modsubi  14093  structcnvcnv  14177  structfun  14178  setsres  14194  strfv  14200  strlemor1  14257  strleun  14260  0rest  14360  firest  14363  restid  14364  prdsval  14385  prdsbas  14387  prdsplusg  14388  prdsmulr  14389  prdsvsca  14390  prdsds  14394  imasaddfnlem  14458  imasvscafn  14467  oppchomfval  14645  oppcbas  14649  2oppchomf  14655  rescbas  14734  rescco  14737  rescabs  14738  idfucl  14783  wunnat  14858  homarel  14896  dmaf  14909  cdaf  14910  catcfuccl  14969  relxpchom  14983  catcxpccl  15009  oppchofcl  15062  oyoncl  15072  odubas  15295  letsr  15389  mgmidmo  15410  releqg  15719  ga0  15807  oppglem  15856  psgnunilem3  15993  psgnunilem4  15994  efgval  16205  efger  16206  efgsp1  16225  efgsfo  16227  efgredleme  16231  efgredlem  16235  efgred  16236  cygctb  16359  gsum2d2lem  16453  gsum2d2  16454  gsumcom2  16455  dprd2d2  16531  pgpfaclem1  16570  mgplem  16584  mgpress  16590  opprlem  16708  reldvdsr  16724  00lsp  17039  sralem  17235  srasca  17239  sravsca  17240  psrvscafval  17438  opsrbaslem  17534  psrbag0  17551  00ply1bas  17670  ply1plusgfvi  17672  nn0srg  17856  rge0srg  17857  zlmsca  17927  znbaslem  17946  resubdrg  18013  ocvfval  18066  ocv0  18077  cssval  18082  thlbas  18096  thlle  18097  islinds2  18217  matsca  18291  m2detleib  18412  eltopspOLD  18498  tgdom  18558  tgidm  18560  indistps2ALT  18593  restbas  18737  resttopon  18740  rest0  18748  leordtval2  18791  iocpnfordt  18794  icomnfordt  18795  iooordt  18796  cnpfval  18813  iscnp2  18818  ist1-3  18928  1stcfb  19024  islly2  19063  1stckgen  19102  ptbasfi  19129  xkotf  19133  dfac14  19166  opnfbas  19390  hauspwpwf1  19535  alexsubALTlem4  19597  alexsubALT  19598  ptcmplem5  19603  cnextrel  19610  ust0  19769  tuslem  19817  0met  19916  prdsdsf  19917  prdsxmetlem  19918  prdsmet  19920  setsmsbas  20025  setsmsds  20026  prdsbl  20041  tngds  20209  qtopbaslem  20312  xrtgioo  20358  xrsdsre  20362  zcld  20365  recld2  20366  sszcld  20369  reperflem  20370  retopcon  20381  iccpnfcnv  20491  bndth  20505  ishtpy  20519  nmoleub2lem2  20646  recmet  20809  resscdrg  20845  ishl2  20857  recms  20859  ehlbase  20885  volf  20987  iundisj2  21005  volsup  21012  icombl  21020  ioombl  21021  ismbf3d  21107  0plef  21125  0pledm  21126  itg1ge0  21139  mbfi1fseqlem5  21172  itg2addlem  21211  iblcnlem1  21240  reldv  21320  limciun  21344  dvexp  21402  dveflem  21426  lhop1lem  21460  lhop  21463  elply2  21639  elplyd  21645  ply1term  21647  ply0  21651  plymullem  21659  qaa  21764  pserulm  21862  pserdvlem2  21868  efcn  21883  sincosq1lem  21934  tangtx  21942  sincos4thpi  21950  sincos6thpi  21952  pige3  21954  efif1olem4  21976  logf1o  21991  relogf1o  21993  log1  22009  loge  22010  relogiso  22021  dvrelog  22057  relogcn  22058  logcn  22067  cxpcn3  22161  resqrcn  22162  leibpi  22312  log2ublem1  22316  birthday  22323  emcllem5  22368  harmonicbnd  22372  harmonicbnd2  22373  emgt0  22375  harmonicbnd3  22376  ppiltx  22490  ppiublem1  22516  ppiub  22518  bclbnd  22594  bpos1lem  22596  bposlem8  22605  lgsquadlem2  22669  2sqlem9  22687  2sqlem10  22688  chebbnd1  22696  selberg2lem  22774  pntrsumo1  22789  selbergsb  22799  pntpbnd  22812  ttgval  23072  ttglem  23073  cchhllem  23084  ax5seglem7  23132  axlowdimlem4  23142  axlowdimlem6  23144  axlowdimlem7  23145  axlowdimlem10  23148  axlowdimlem13  23151  axlowdimlem16  23154  axlowdimlem17  23155  axlowdim  23158  uhgra0  23194  umgra0  23210  usgra0  23240  usgra1v  23259  cusgraexilem2  23326  cusgrasizeindslem2  23333  0wlk  23395  0trl  23396  wlkntrllem2  23410  wlkntrl  23412  0pth  23420  1pthonlem1  23439  usgrcyclnl2  23478  4cycl4dv  23504  vdgrf  23519  umgrabi  23555  vdegp1ai  23556  vdegp1bi  23557  konigsberg  23559  ex-dif  23581  ex-in  23583  ex-eprel  23591  ex-id  23592  ex-fl  23605  avril1  23607  2bornot2b  23608  grposn  23653  issubgoi  23748  0vfval  23935  vsfval  23964  ajmoi  24210  ajfuni  24211  normlem2  24464  norm3adifii  24501  hhip  24530  hlim0  24589  hlimcaui  24590  hlimf  24591  hhssnv  24616  shscli  24671  shsval2i  24741  h1de2i  24907  fh3i  24977  fh4i  24978  cm2mi  24980  qlaxr3i  24990  mayetes3i  25084  ho0f  25106  hoif  25109  hodidi  25142  ho0subi  25150  hosd1i  25177  adjmo  25187  nmopsetn0  25220  nmfnsetn0  25233  funadj  25241  funcnvadj  25248  nmcexi  25381  cnlnadjlem8  25429  nmoptri2i  25454  opsqrlem4  25498  hmopidmchi  25506  pjoci  25535  pjinvari  25546  abrexdomjm  25839  elim2ifim  25858  iundisj2f  25883  rinvf1o  25900  funcnvmptOLD  25937  dfcnv2  25945  snct  25962  dmct  25965  fpwrelmap  25984  iundisj2fi  26032  gsumle  26197  reofld  26260  rearchi  26262  xrge0slmod  26264  xrge0iifcnv  26315  xrge0pluscn  26322  zlmds  26345  zlmtset  26346  cnzh  26351  rezh  26352  qqhre  26398  esumfsup  26471  esumpcvgval  26479  hasheuni  26486  esumcvg  26487  dmsigagen  26539  measvuni  26580  voliune  26597  volfiniune  26598  ddemeas  26604  br2base  26636  dya2iocuni  26650  oms0  26662  eulerpartlem1  26702  eulerpartlemt  26706  eulerpartgbij  26707  fib0  26734  fib6  26741  coinfliprv  26817  ballotlem2  26823  ballotlemfc0  26827  ballotlemfcc  26828  ballotlemic  26841  ballotlem7  26870  ballotth  26872  plymul02  26899  signswmnd  26910  lgamgulm2  26974  lgamcvglem  26978  gamf  26981  subfacp1lem5  27024  subfacp1lem6  27025  kur14lem9  27054  cvmcov2  27116  cvmliftlem1  27126  cvmliftlem4  27129  cvmliftlem5  27130  problem5  27254  ghomgrpilem2  27256  relexp0  27282  relexpsucr  27283  relexpsucl  27285  dfrtrclrec2  27296  rtrclreclem.refl  27297  rtrclreclem.subset  27298  rtrclreclem.min  27300  dfrtrcl2  27301  brtpid1  27328  brtpid2  27329  brtpid3  27330  fzp1nel  27348  fprodcom2  27446  faclimlem1  27500  domep  27557  axextndbi  27569  poseq  27665  wfrlem6  27680  wfrlem14  27688  wfrlem16  27690  frrlem10  27730  sltval2  27748  nosgnn0i  27751  brv  27859  txprel  27861  relsset  27870  relbigcup  27879  fvbigcup  27884  fnsingle  27901  fvsingle  27902  snelsingles  27904  funimage  27910  fullfunfnv  27928  imagesset  27935  funtransport  28013  colinrel  28039  funray  28122  funline  28124  bpolylem  28142  bpoly3  28152  bpoly4  28153  0hf  28166  waj-ax  28212  lukshef-ax2  28213  arg-ax  28214  limsucncmpi  28243  mblfinlem1  28381  mblfinlem2  28382  ismblfin  28385  voliunnfl  28388  cnambfre  28393  dvtanlem  28394  comppfsc  28532  neibastop2lem  28534  filnetlem3  28554  cover2  28560  abrexdom  28577  fdc  28594  cncfres  28617  heibor1lem  28661  bicontr  28833  an12i  28854  tsim1  28894  ac6s6f  28938  moxfr  28981  mapfzcons1  29006  diophrw  29050  0dioph  29070  vdioph  29071  rabren3dioph  29107  2nn0ind  29239  rpnnen3  29334  kelac2lem  29370  frlmpwfi  29406  lhe4.4ex1a  29556  rusbcALT  29646  ipo0  29658  ifr0  29659  fnchoice  29704  stoweidlem13  29761  stoweidlem34  29782  stirlinglem5  29826  stirlinglem13  29834  stirlingr  29838  aistia  29864  aisfina  29865  aiffnbandciffatnotciffb  29871  axorbciffatcxorb  29872  abnotbtaxb  29883  abnotataxb  29884  usgra2pthspth  30248  usgra2pthlem1  30253  wwlknext  30309  wwlknfi  30323  disjxwwlkn  30517  frgra0  30539  numclwwlkdisj  30626  numclwwlk3lem  30654  eliunxp2  30673  pmtrsn  30721  fsuppmapnn0fz  30746  zlmodzxzldeplem  30929  zlmodzxzldep  30935  ldepslinc  30940  ex-gte  30953  AnelBC  30988  empty-surprise  31021  eximp-surprise2  31024  vk15.4j  31120  2sb5nd  31156  dfvd1ir  31173  dfvd2anir  31184  dfvd2ir  31186  dfvd3ir  31193  dfvd3anir  31196  iden2  31223  e0bir  31397  uun2221p1  31434  uun2221p2  31435  2sb5ndVD  31533  2sb5ndALT  31555  iunconlem2  31558  bnj226  31612  bnj1101  31665  bnj110  31738  bnj149  31755  bnj150  31756  bnj151  31757  bnj517  31765  bnj580  31793  bnj865  31803  bnj900  31809  bnj996  31835  bnj1110  31860  bnj1133  31867  bnj1128  31868  bnj1145  31871  bnj1137  31873  bnj1171  31878  bnj1176  31883  bj-babylob  32003  bj-nfv  32042  bj-nalnalimiOLD  32045  bj-dvdemo1  32180  bj-disjcsn  32287  bj-snsetex  32303  bj-0eltag  32318  bj-2upln0  32363  bj-2upln1upl  32364  elimhyps  32452  dedths  32453  renegclALT  32454  hlhilslem  35426