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  698  stabnot  841  mpbir2an  951  mpbir3an  1206  tru  1402  dcfromnotnotr  1493  dcfromcon  1494  dcfrompeirce  1495  mpgbir  1502  nfxfr  1523  19.8a  1639  sbt  1833  dveeq2  1864  dveeq2or  1865  sbequilem  1887  cbvex2  1972  dvelimALT  2064  dvelimfv  2065  dvelimor  2072  nfeuv  2098  moaneu  2157  moanmo  2158  eqeltri  2305  nfcxfr  2381  neir  2415  neirr  2421  eqnetri  2435  nesymir  2459  nelir  2510  mprgbir  2600  vex  2816  issetri  2823  moeq  2992  cdeqi  3027  ru  3041  eqsstri  3270  3sstr4i  3279  mosn  3725  rabrsndc  3759  tpid1  3803  tpid2  3805  tpid3  3808  pwv  3913  uni0  3941  eqbrtri  4130  tr0  4219  trv  4220  zfnuleu  4234  0ex  4237  inex1  4244  elpwi2  4270  0elpw  4277  axpow2  4289  axpow3  4290  vpwex  4292  zfpair2  4323  exss  4343  opwo0id  4365  moop2  4368  pwundifss  4406  po0  4432  epse  4463  fr0  4472  0elon  4513  onm  4522  uniex2  4557  snnex  4569  ordtriexmidlem  4641  ordtriexmid  4643  ontr2exmid  4647  ordtri2or2exmidlem  4648  onsucsssucexmid  4649  onsucelsucexmidlem  4651  ruALT  4673  zfregfr  4696  dcextest  4703  zfinf2  4711  omex  4715  finds  4722  finds2  4723  ordom  4729  omsinds  4744  relsnop  4856  relxp  4859  rel0  4877  relopabiv  4878  relopabi  4880  eliunxp  4894  opeliunxp2  4895  dmi  4971  xpidtr  5153  cnvcnv  5215  dmsn0  5230  cnvsn0  5231  funmpt  5390  funmpt2  5391  funinsn  5405  isarep2  5443  f0  5558  f10  5649  f10d  5650  f1o00  5651  f1oi  5654  f1osn  5656  brprcneu  5663  fvopab3ig  5751  opabex  5910  eufnfv  5917  mpofun  6155  reldmmpo  6165  ovid  6170  ovidig  6171  ovidi  6172  ovig  6175  ovi3  6191  relmptopab  6256  oprabex  6321  oprabex3  6322  f1stres  6353  f2ndres  6354  opeliunxp2f  6469  tpos0  6505  issmo  6519  tfrlem6  6547  tfrlem8  6549  tfri1dALT  6582  tfrcl  6595  rdgfun  6604  frecfun  6626  frecfcllem  6635  0lt1o  6673  eqer  6799  ecopover  6867  ecopoverg  6870  th3qcor  6873  mapsnf1o3  6932  ssdomg  7018  ensn1  7036  xpcomf1o  7076  fiunsnnn  7138  finexdc  7160  elssdc  7162  exmidpw  7168  fissfi  7216  dcfi  7268  omct  7408  infnninf  7415  infnninfOLD  7416  pm54.43  7487  exmidonfinlem  7496  pw1on  7536  pw1dom2  7537  pw1ne1  7539  2oneel  7570  dmaddpi  7640  dmmulpi  7641  1lt2pi  7655  indpi  7657  1lt2nq  7721  genpelxp  7826  ltexprlempr  7923  recexprlempr  7947  cauappcvgprlemcl  7968  cauappcvgprlemladd  7973  caucvgprlemcl  7991  caucvgprprlemcl  8019  m1p1sr  8075  m1m1sr  8076  0lt1sr  8080  peano1nnnn  8167  ax1cn  8176  ax1re  8177  axaddf  8183  axmulf  8184  ax0lt1  8191  0lt1  8400  subaddrii  8562  ixi  8857  1ap0  8864  sup3exmid  9231  nn1suc  9256  neg1lt0  9345  4d2e2  9398  iap0  9461  un0mulcl  9530  pnf0xnn0  9570  3halfnz  9675  nummac  9753  uzf  9856  mnfltpnf  10118  ixxf  10231  ioof  10304  fzf  10346  fzp1disj  10414  fzp1nel  10438  fzo0  10504  frecfzennn  10788  frechashgf1o  10790  xnn0nnen  10799  fxnn0nninf  10801  seq3f1olemp  10877  sq0  10992  irec  11001  hash0  11159  prhash2ex  11174  hashfibclem  11206  climmo  11983  sum0  12074  fisumcom2  12124  prod0  12271  fprodcom2fi  12312  cos1bnd  12445  cos2bnd  12446  3dvds  12550  n2dvdsm1  12599  n2dvds3  12601  flodddiv4  12622  3lcm2e6woprm  12783  6lcm4e12  12784  2prm  12824  3lcm2e6  12857  pockthi  13056  modsubi  13117  ballotfilem2  13142  unennn  13148  ssnnctlemct  13197  structcnvcnv  13228  strleun  13317  starvndxnbasendx  13355  starvndxnplusgndx  13356  starvndxnmulrndx  13357  scandxnbasendx  13367  scandxnplusgndx  13368  scandxnmulrndx  13369  vscandxnbasendx  13372  vscandxnplusgndx  13373  vscandxnmulrndx  13374  vscandxnscandx  13375  ipndxnbasendx  13385  ipndxnplusgndx  13386  ipndxnmulrndx  13387  slotsdifipndx  13388  tsetndxnplusgndx  13405  tsetndxnmulrndx  13406  tsetndxnstarvndx  13407  slotstnscsi  13408  plendxnplusgndx  13419  plendxnmulrndx  13420  plendxnscandx  13421  plendxnvscandx  13422  slotsdifplendx  13423  basendxnocndx  13426  plendxnocndx  13427  dsndxnplusgndx  13434  dsndxnmulrndx  13435  slotsdnscsi  13436  dsndxntsetndx  13437  slotsdifdsndx  13438  unifndxntsetndx  13444  slotsdifunifndx  13445  restid  13463  prdsval  13486  mgmidmo  13585  reldvdsr  14236  rrgmex  14406  lssmex  14503  lidlmex  14623  2idlmex  14649  fczpsrbag  14820  tgdom  14937  tgidm  14939  resttopon  15036  rest0  15044  psmetrel  15187  metrel  15207  xmetrel  15208  xmetf  15215  0met  15249  mopnrel  15306  setsmsbasg  15344  setsmsdsg  15345  qtopbasss  15386  reldvg  15544  dvexp  15576  dveflem  15591  elply2  15600  elplyd  15606  ply1term  15608  plymullem  15615  efcn  15633  sinhalfpilem  15656  sincosq1lem  15690  tangtx  15703  sincos4thpi  15705  pigt3  15709  dfrelog  15725  relogf1o  15726  log1  15731  loge  15732  relogiso  15738  2logb9irr  15836  2logb9irrap  15842  2sqlem9  15997  2sqlem10  15998  uhgr0e  16077  uhgr0  16080  umgrbien  16105  usgr0  16234  griedg0prc  16245  1loopgruspgr  16298  konigsbergumgr  16482  konigsberglem1  16483  ex-fl  16493  bj-nndcALT  16530  bj-axempty  16663  bj-axempty2  16664  bdinex1  16669  bj-zfpair2  16680  bj-uniex2  16686  bj-indint  16701  bj-omind  16704  bj-omex  16712  bj-omelon  16731  pw1ndom3  16764  0nninf  16782  dceqnconst  16846  dcapnconst  16847  gfsum0  16864