Theorem mpbir 146

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

Syntax hints:   <-> wb 105

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  pm5.74ri  181  imnani  695  stabnot  838  mpbir2an  948  mpbir3an  1203  tru  1399  dcfromnotnotr  1490  dcfromcon  1491  dcfrompeirce  1492  mpgbir  1499  nfxfr  1520  19.8a  1636  sbt  1830  dveeq2  1861  dveeq2or  1862  sbequilem  1884  cbvex2  1969  dvelimALT  2061  dvelimfv  2062  dvelimor  2069  nfeuv  2095  moaneu  2154  moanmo  2155  eqeltri  2302  nfcxfr  2369  neir  2403  neirr  2409  eqnetri  2423  nesymir  2447  nelir  2498  mprgbir  2588  vex  2803  issetri  2810  moeq  2979  cdeqi  3014  ru  3028  eqsstri  3257  3sstr4i  3266  mosn  3703  rabrsndc  3735  tpid1  3779  tpid2  3781  tpid3  3784  pwv  3888  uni0  3916  eqbrtri  4105  tr0  4194  trv  4195  zfnuleu  4209  0ex  4212  inex1  4219  elpwi2  4244  0elpw  4250  axpow2  4262  axpow3  4263  vpwex  4265  zfpair2  4296  exss  4315  opwo0id  4337  moop2  4340  pwundifss  4378  po0  4404  epse  4435  fr0  4444  0elon  4485  onm  4494  uniex2  4529  snnex  4541  ordtriexmidlem  4613  ordtriexmid  4615  ontr2exmid  4619  ordtri2or2exmidlem  4620  onsucsssucexmid  4621  onsucelsucexmidlem  4623  ruALT  4645  zfregfr  4668  dcextest  4675  zfinf2  4683  omex  4687  finds  4694  finds2  4695  ordom  4701  omsinds  4716  relsnop  4828  relxp  4831  rel0  4848  relopabiv  4849  relopabi  4851  eliunxp  4865  opeliunxp2  4866  dmi  4942  xpidtr  5123  cnvcnv  5185  dmsn0  5200  cnvsn0  5201  funmpt  5360  funmpt2  5361  funinsn  5374  isarep2  5412  f0  5522  f10  5612  f10d  5613  f1o00  5614  f1oi  5617  f1osn  5619  brprcneu  5626  fvopab3ig  5714  opabex  5871  eufnfv  5878  mpofun  6116  reldmmpo  6126  ovid  6131  ovidig  6132  ovidi  6133  ovig  6136  ovi3  6152  relmptopab  6217  oprabex  6283  oprabex3  6284  f1stres  6315  f2ndres  6316  opeliunxp2f  6397  tpos0  6433  issmo  6447  tfrlem6  6475  tfrlem8  6477  tfri1dALT  6510  tfrcl  6523  rdgfun  6532  frecfun  6554  frecfcllem  6563  0lt1o  6601  eqer  6727  ecopover  6795  ecopoverg  6798  th3qcor  6801  mapsnf1o3  6859  ssdomg  6945  ensn1  6963  xpcomf1o  7002  fiunsnnn  7061  finexdc  7083  elssdc  7085  exmidpw  7091  dcfi  7169  omct  7305  infnninf  7312  infnninfOLD  7313  pm54.43  7384  exmidonfinlem  7392  pw1on  7432  pw1dom2  7433  pw1ne1  7435  2oneel  7463  dmaddpi  7533  dmmulpi  7534  1lt2pi  7548  indpi  7550  1lt2nq  7614  genpelxp  7719  ltexprlempr  7816  recexprlempr  7840  cauappcvgprlemcl  7861  cauappcvgprlemladd  7866  caucvgprlemcl  7884  caucvgprprlemcl  7912  m1p1sr  7968  m1m1sr  7969  0lt1sr  7973  peano1nnnn  8060  ax1cn  8069  ax1re  8070  axaddf  8076  axmulf  8077  ax0lt1  8084  0lt1  8294  subaddrii  8456  ixi  8751  1ap0  8758  sup3exmid  9125  nn1suc  9150  neg1lt0  9239  4d2e2  9292  iap0  9355  un0mulcl  9424  pnf0xnn0  9460  3halfnz  9565  nummac  9643  uzf  9746  mnfltpnf  10008  ixxf  10121  ioof  10194  fzf  10235  fzp1disj  10303  fzp1nel  10327  fzo0  10393  frecfzennn  10676  frechashgf1o  10678  xnn0nnen  10687  fxnn0nninf  10689  seq3f1olemp  10765  sq0  10880  irec  10889  hash0  11046  prhash2ex  11060  climmo  11846  sum0  11936  fisumcom2  11986  prod0  12133  fprodcom2fi  12174  cos1bnd  12307  cos2bnd  12308  3dvds  12412  n2dvdsm1  12461  n2dvds3  12463  flodddiv4  12484  3lcm2e6woprm  12645  6lcm4e12  12646  2prm  12686  3lcm2e6  12719  pockthi  12918  modsubi  12979  unennn  13005  ssnnctlemct  13054  structcnvcnv  13085  strleun  13174  starvndxnbasendx  13212  starvndxnplusgndx  13213  starvndxnmulrndx  13214  scandxnbasendx  13224  scandxnplusgndx  13225  scandxnmulrndx  13226  vscandxnbasendx  13229  vscandxnplusgndx  13230  vscandxnmulrndx  13231  vscandxnscandx  13232  ipndxnbasendx  13242  ipndxnplusgndx  13243  ipndxnmulrndx  13244  slotsdifipndx  13245  tsetndxnplusgndx  13262  tsetndxnmulrndx  13263  tsetndxnstarvndx  13264  slotstnscsi  13265  plendxnplusgndx  13276  plendxnmulrndx  13277  plendxnscandx  13278  plendxnvscandx  13279  slotsdifplendx  13280  basendxnocndx  13283  plendxnocndx  13284  dsndxnplusgndx  13291  dsndxnmulrndx  13292  slotsdnscsi  13293  dsndxntsetndx  13294  slotsdifdsndx  13295  unifndxntsetndx  13301  slotsdifunifndx  13302  restid  13320  prdsval  13343  mgmidmo  13442  reldvdsr  14092  rrgmex  14262  lssmex  14356  lidlmex  14476  2idlmex  14502  fczpsrbag  14672  tgdom  14783  tgidm  14785  resttopon  14882  rest0  14890  psmetrel  15033  metrel  15053  xmetrel  15054  xmetf  15061  0met  15095  mopnrel  15152  setsmsbasg  15190  setsmsdsg  15191  qtopbasss  15232  reldvg  15390  dvexp  15422  dveflem  15437  elply2  15446  elplyd  15452  ply1term  15454  plymullem  15461  efcn  15479  sinhalfpilem  15502  sincosq1lem  15536  tangtx  15549  sincos4thpi  15551  pigt3  15555  dfrelog  15571  relogf1o  15572  log1  15577  loge  15578  relogiso  15584  2logb9irr  15682  2logb9irrap  15688  2sqlem9  15840  2sqlem10  15841  uhgr0e  15919  uhgr0  15922  umgrbien  15947  usgr0  16074  griedg0prc  16085  ex-fl  16231  bj-nndcALT  16264  bj-axempty  16398  bj-axempty2  16399  bdinex1  16404  bj-zfpair2  16415  bj-uniex2  16421  bj-indint  16436  bj-omind  16439  bj-omex  16447  bj-omelon  16466  pw1ndom3  16499  0nninf  16516  dceqnconst  16574  dcapnconst  16575