Theorem mpbir 201

Description: An inference from a biconditional, related to modus ponens. (Contributed by NM, 5-Aug-1993.)

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

Syntax hints:   <-> wb 177

This theorem is referenced by:  pm5.74ri  238  con4bii  289  orri  366  imorri  404  imnani  413  mpbir2an  887  mpbir3an  1136  tru  1327  nic-mpALT  1443  nic-ax  1444  nic-axALT  1445  mpto2OLD  1541  mtp-xor  1542  mtp-xorOLD  1543  mpgbir  1556  nfxfr  1576  19.35ri  1609  a9ev  1664  exiftruOLD  1666  exan  1899  ax12  1985  a9eOLD  2000  cbval2  2054  cbvex2  2055  sbt  2082  moaneu  2313  moanmo  2314  axi12  2383  axext2  2386  eqeltri  2474  nfcxfr  2537  neirr  2572  exmidne  2573  eqnetri  2584  mprgbir  2736  vex  2919  issetri  2923  moeq  3070  cdeqi  3106  ru  3120  eqsstri  3338  3sstr4i  3347  tpid1  3877  tpid2  3878  tpid3  3880  pwv  3974  uni0  4002  eqbrtri  4191  tr0  4273  trv  4274  zfrep4  4288  zfnuleu  4295  axnulALT  4296  0ex  4299  inex1  4304  0elpw  4329  axpow2  4339  axpow3  4340  pwex  4342  dvdemo1  4359  zfpair2  4364  exss  4386  moop2  4411  pwundif  4450  po0  4478  epse  4525  0elon  4594  nsuceq0  4621  uniex2  4663  snnex  4672  tfinds2  4802  finds  4830  finds2  4832  relsnop  4939  relxp  4942  rel0  4958  relopabi  4959  eliunxp  4971  opeliunxp2  4972  dmi  5043  xpidtr  5215  xpima  5272  cnvcnv  5282  dmsn0  5296  cnvsn0  5297  funmpt  5448  funmpt2  5449  isarep2  5492  fresaunres2  5574  f0  5586  f10  5668  f1o00  5669  f1oi  5672  f1osn  5674  brprcneu  5680  fvopab3ig  5762  opabex  5923  eufnfv  5931  mpt2fun  6131  reldmmpt2  6140  oprabex  6146  oprabex3  6147  ovid  6149  ovidig  6150  ovidi  6151  ovig  6154  ov3  6169  caovmo  6243  relmptopab  6251  f1stres  6327  f2ndres  6328  relmpt2opab  6388  tpos0  6468  porpss  6485  opabiotafun  6495  canth  6498  ncanth  6499  issmo  6569  tfrlem6  6602  tfrlem8  6604  tfrlem16  6613  tfr1a  6614  tfr1  6617  tz7.44lem1  6622  seqomlem2  6667  seqomlem3  6668  seqomlem4  6669  fnseqom  6671  abianfp  6675  0lt1o  6707  0we1  6709  eqer  6897  ecopover  6967  th3qcor  6971  mapsnf1o3  7021  ssdomg  7112  ensn1  7130  snfi  7146  xpcomf1o  7156  map2xp  7236  limensuci  7242  sdom1  7267  unblem4  7321  fidomdm  7347  marypha1lem  7396  hartogslem1  7467  hartogs  7469  card2on  7478  ruv  7524  ruALT  7525  inf2  7534  inf3lem6  7544  infeq5i  7547  zfinf2  7553  cantnflt  7583  cantnf  7605  mapfien  7609  cnfcom  7613  trcl  7620  tz9.1c  7622  tc2  7637  r1funlim  7648  r1fnon  7649  karden  7775  tskwe  7793  cardprclem  7822  cardprc  7823  pm54.43  7843  r0weon  7850  iunmapdisj  7860  alephfnon  7902  alephfplem4  7944  alephfp  7945  alephval3  7947  aceq3lem  7957  kmlem2  7987  cda1dif  8012  ackbij1  8074  ackbij2lem2  8076  ackbij2  8079  infpssrlem3  8141  hsmexlem4  8265  hsmexlem5  8266  axdc3lem4  8289  ac2  8297  axac3  8300  ac6  8316  axdclem2  8356  ondomon  8394  alephsucpw  8401  pwcfsdom  8414  cfpwsdom  8415  smobeth  8417  axpowndlem3  8430  zfcndun  8446  zfcndpow  8447  zfcndinf  8449  zfcndac  8450  wunex2  8569  uniwun  8571  wuncval2  8578  grur1  8651  axgroth5  8655  axgroth2  8656  axgroth6  8659  axgroth3  8662  grothtsk  8666  inaprc  8667  ltsopi  8721  dmaddpi  8723  dmmulpi  8724  1lt2pi  8738  nqerf  8763  addnqf  8781  mulnqf  8782  1lt2nq  8806  m1p1sr  8923  m1m1sr  8924  0lt1sr  8926  axaddf  8976  axmulf  8977  ax1cn  8980  ax1ne0  8991  pnfnre  9083  mnfnre  9084  subaddrii  9345  ine0  9425  ixi  9607  recgt0ii  9872  nn1suc  9977  4d2e2  10088  nnunb  10173  arch  10174  un0mulcl  10210  nummac  10370  uzf  10447  indstr  10501  mnfltpnf  10679  ixxf  10882  ioof  10958  fzf  11003  fzp1disj  11061  fzof  11092  om2uzrani  11247  om2uzf1oi  11248  uzrdglem  11252  uzrdgfni  11253  uzrdg0i  11254  ltwenn  11257  hashgf1o  11265  axdc4uzlem  11276  sq0  11428  irec  11435  hashkf  11575  hashf  11580  hash0  11601  hashsslei  11640  hashxplem  11651  hashbclem  11656  hashf1lem1  11659  wrd0  11687  wrdexg  11694  revs1  11752  cats1fvn  11777  climmo  12306  fsumcom2  12513  ackbijnn  12562  incexclem  12571  infcvgaux1i  12591  efcvgfsum  12643  cos1bnd  12743  cos2bnd  12744  eirr  12759  znnen  12767  qnnen  12768  aleph1re  12799  sqr2irr  12803  nthruz  12806  dvdslelem  12849  3dvds  12867  divalglem5  12872  bitsf  12894  sadcaddlem  12924  sadadd2lem  12926  sadadd3  12928  sadaddlem  12933  isprm3  13043  2prm  13050  phicl2  13112  pockthi  13230  unbenlem  13231  prmrec  13245  vdwlem13  13316  vdwnn  13321  ramcl2  13339  mod2xnegi  13362  modsubi  13363  structcnvcnv  13435  structfun  13436  setsres  13450  strfv  13456  strlemor1  13511  strleun  13514  0rest  13612  firest  13615  restid  13616  prdsval  13633  prdsbas  13635  prdsplusg  13636  prdsmulr  13637  prdsvsca  13638  prdsds  13641  imasaddfnlem  13708  imasvscafn  13717  oppchomfval  13895  oppcbas  13899  2oppchomf  13905  rescbas  13984  rescco  13987  rescabs  13988  idfucl  14033  wunnat  14108  homarel  14146  dmaf  14159  cdaf  14160  catcfuccl  14219  relxpchom  14233  catcxpccl  14259  oppchofcl  14312  oyoncl  14322  odubas  14515  letsr  14627  mgmidmo  14648  releqg  14942  ga0  15030  oppglem  15101  efgval  15304  efger  15305  efgsp1  15324  efgsfo  15326  efgredleme  15330  efgredlem  15334  efgred  15335  cygctb  15456  gsum2d2lem  15502  gsum2d2  15503  gsumcom2  15504  dprd2d2  15557  pgpfaclem1  15594  mgplem  15608  mgpress  15614  opprlem  15688  reldvdsr  15704  00lsp  16012  sralem  16204  srasca  16208  psrvscafval  16409  opsrbaslem  16493  psrbag0  16509  00ply1bas  16589  ply1plusgfvi  16591  zlmsca  16757  znbaslem  16774  ocvfval  16848  ocv0  16859  cssval  16864  thlbas  16878  thlle  16879  eltopspOLD  16938  tgdom  16998  tgidm  17000  indistps2ALT  17033  restbas  17176  resttopon  17179  rest0  17187  leordtval2  17230  iocpnfordt  17233  icomnfordt  17234  iooordt  17235  cnpfval  17252  iscnp2  17257  ist1-3  17367  1stcfb  17461  islly2  17500  1stckgen  17539  ptbasfi  17566  xkotf  17570  dfac14  17603  opnfbas  17827  zfbas  17881  hauspwpwf1  17972  alexsubALTlem4  18034  alexsubALT  18035  ptcmplem5  18040  cnextrel  18047  ust0  18202  tuslem  18250  0met  18349  prdsdsf  18350  prdsxmetlem  18351  prdsmet  18353  setsmsbas  18458  setsmsds  18459  prdsbl  18474  tngds  18642  qtopbaslem  18745  xrtgioo  18790  xrsdsre  18794  zcld  18797  recld2  18798  sszcld  18801  reperflem  18802  retopcon  18813  iccpnfcnv  18922  bndth  18936  ishtpy  18950  nmoleub2lem2  19077  recmet  19229  resscdrg  19265  ishl2  19277  volf  19378  iundisj2  19396  volsup  19403  icombl  19411  ioombl  19412  ismbf3d  19499  0plef  19517  0pledm  19518  itg1ge0  19531  mbfi1fseqlem5  19564  itg2addlem  19603  iblcnlem1  19632  reldv  19710  limciun  19734  dvexp  19792  dveflem  19816  lhop1lem  19850  lhop  19853  elply2  20068  elplyd  20074  ply1term  20076  ply0  20080  plymullem  20088  qaa  20193  aaliou3  20221  pserulm  20291  pserdvlem2  20297  efcn  20312  sincosq1lem  20358  tangtx  20366  sincos4thpi  20374  sincos6thpi  20376  pige3  20378  efif1olem4  20400  logf1o  20415  relogf1o  20417  log1  20433  loge  20434  relogiso  20445  dvrelog  20481  relogcn  20482  logcn  20491  cxpcn3  20585  resqrcn  20586  leibpi  20735  log2ublem1  20739  birthday  20746  emcllem5  20791  harmonicbnd  20795  harmonicbnd2  20796  emgt0  20798  harmonicbnd3  20799  ppiltx  20913  ppiublem1  20939  ppiub  20941  bclbnd  21017  bpos1lem  21019  bposlem8  21028  lgsquadlem2  21092  2sqlem9  21110  2sqlem10  21111  chebbnd1  21119  selberg2lem  21197  pntrsumo1  21212  selbergsb  21222  pntpbnd  21235  uhgra0  21297  umgra0  21313  usgra0  21343  usgra1v  21362  cusgraexilem2  21429  cusgrasizeindslem2  21436  0wlk  21498  0trl  21499  wlkntrllem2  21513  wlkntrl  21515  0pth  21523  1pthonlem1  21542  usgrcyclnl2  21581  4cycl4dv  21607  vdgrf  21622  umgrabi  21658  vdegp1ai  21659  vdegp1bi  21660  konigsberg  21662  ex-dif  21684  ex-in  21686  ex-eprel  21694  ex-id  21695  ex-fl  21708  avril1  21710  2bornot2b  21711  grposn  21756  issubgoi  21851  0vfval  22038  vsfval  22067  ajmoi  22313  ajfuni  22314  normlem2  22566  norm3adifii  22603  hhip  22632  hlim0  22691  hlimcaui  22692  hlimf  22693  hhssnv  22717  shscli  22772  shsval2i  22842  h1de2i  23008  fh3i  23078  fh4i  23079  cm2mi  23081  qlaxr3i  23091  mayetes3i  23185  ho0f  23207  hoif  23210  hodidi  23243  ho0subi  23251  hosd1i  23278  adjmo  23288  nmopsetn0  23321  nmfnsetn0  23334  funadj  23342  funcnvadj  23349  nmcexi  23482  cnlnadjlem8  23530  nmoptri2i  23555  opsqrlem4  23599  hmopidmchi  23607  pjoci  23636  pjinvari  23647  abrexdomjm  23941  elim2ifim  23959  iundisj2f  23983  rinvf1o  23995  funcnvmptOLD  24035  snct  24056  dmct  24059  iundisj2fi  24106  xrge0iifcnv  24272  xrge0pluscn  24279  recms  24296  zlmds  24301  zlmtset  24302  cnzh  24307  rezh  24308  qqhre  24339  esumfsup  24413  esumpcvgval  24421  hasheuni  24428  esumcvg  24429  dmsigagen  24480  measvuni  24521  voliune  24538  volfiniune  24539  br2base  24572  dya2iocuni  24586  coinfliprv  24693  ballotlem2  24699  ballotlemfc0  24703  ballotlemfcc  24704  ballotlemic  24717  ballotlem7  24746  ballotth  24748  lgamgulm2  24773  lgamcvglem  24777  gamf  24780  subfacp1lem5  24823  subfacp1lem6  24824  kur14lem9  24853  cvmcov2  24915  cvmliftlem1  24925  cvmliftlem4  24928  cvmliftlem5  24929  ghomgrpilem2  25050  relexp0  25082  relexpsucr  25083  relexpsucl  25085  dfrtrclrec2  25096  rtrclreclem.refl  25097  rtrclreclem.subset  25098  rtrclreclem.min  25100  dfrtrcl2  25101  brtpid1  25131  brtpid2  25132  brtpid3  25133  fzp1nel  25163  fprodcom2  25261  faclimlem1  25310  domep  25363  axextndbi  25375  poseq  25467  wfrlem14  25483  wfrlem16  25485  frrlem10  25506  sltval2  25524  nosgnn0i  25527  brv  25631  txprel  25633  relsset  25642  relbigcup  25651  fvbigcup  25656  fnsingle  25672  fvsingle  25673  snelsingles  25675  funimage  25681  fullfunfnv  25699  ax5seglem7  25778  axlowdimlem4  25788  axlowdimlem6  25790  axlowdimlem7  25791  axlowdimlem10  25794  axlowdimlem13  25797  axlowdimlem16  25800  axlowdimlem17  25801  axlowdim  25804  funtransport  25869  colinrel  25895  funray  25978  funline  25980  bpolylem  25998  bpoly3  26008  bpoly4  26009  0hf  26022  waj-ax  26068  lukshef-ax2  26069  arg-ax  26070  limsucncmpi  26099  mblfinlem  26143  ismblfin  26146  voliunnfl  26149  cnambfre  26154  comppfsc  26277  neibastop2lem  26279  filnetlem3  26299  cover2  26305  abrexdom  26322  fdc  26339  cncfres  26364  heibor1lem  26408  moxfr  26623  mapfzcons1  26663  diophrw  26707  0dioph  26727  vdioph  26728  rabren3dioph  26766  2nn0ind  26898  rpnnen3  26993  kelac2lem  27030  frlmpwfi  27130  islinds2  27151  psgnunilem3  27287  psgnunilem4  27288  matsca  27338  lhe4.4ex1a  27414  rusbcALT  27507  ipo0  27519  ifr0  27520  fnchoice  27567  stoweidlem13  27629  stoweidlem34  27650  stirlinglem5  27694  stirlinglem13  27702  stirlingr  27706  aistia  27732  aisfina  27733  aiffnbandciffatnotciffb  27739  axorbciffatcxorb  27740  abnotbtaxb  27751  abnotataxb  27752  usgra2pthspth  28035  usgra2pthlem1  28040  frgra0  28098  ex-gte  28186  AnelBC  28221  vk15.4j  28323  2sb5nd  28358  dfvd1ir  28373  dfvd2anir  28385  dfvd2ir  28387  dfvd3ir  28394  dfvd3anir  28397  iden2  28424  e0bir  28598  uun2221p1  28635  uun2221p2  28636  2sb5ndVD  28731  2sb5ndALT  28754  bnj226  28807  bnj1101  28861  bnj110  28935  bnj149  28952  bnj150  28953  bnj151  28954  bnj517  28962  bnj580  28990  bnj865  29000  bnj900  29006  bnj996  29032  bnj1110  29057  bnj1133  29064  bnj1128  29065  bnj1145  29068  bnj1137  29070  bnj1171  29075  bnj1176  29080  a9eNEW7  29176  sbtNEW7  29332  cbval2OLD7  29414  cbvex2OLD7  29415  nfsb4tw2AUXOLD7  29430  hlhilslem  32424

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

This theorem depends on definitions:  df-bi 178