Theorem mpbiri 248

Description: An inference from a nested biconditional, related to modus ponens. (Contributed by NM, 21-Jun-1993.) (Proof shortened by Wolf Lammen, 25-Oct-2012.)

Hypotheses

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

Assertion

Ref	Expression
mpbiri	|- ( ph -> ps )

Proof of Theorem mpbiri

Step	Hyp	Ref	Expression
1		mpbiri.min	. . 3 |- ch
2	1	a1i 11	. 2 |- ( ph -> ch )
3		mpbiri.maj	. 2 |- ( ph -> ( ps <-> ch ) )
4	2, 3	mpbird 247	1 |- ( ph -> ps )

Syntax hints:   -> wi 4   <-> wb 196

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 197

This theorem is referenced by:  dedt  1031  dedtOLD  1034  spei  2261  nfald2  2331  nfabd2  2784  raleleqALT  3157  dedhb  3376  sbceqal  3487  ssdifeq0  4051  r19.2zb  4061  dedth  4139  pwidg  4173  elpr2  4199  elpr2OLD  4200  snidg  4206  exsnrex  4221  ifpr  4233  rabrsn  4259  prid1g  4295  tpid3g  4305  pwpw0  4344  sssn  4358  preqr1OLD  4380  elpreqpr  4396  pwsnALT  4429  unimax  4473  intmin3  4505  syl6eqbr  4692  intabs  4825  pwnss  4830  0inp0  4837  copsexg  4956  euotd  4975  elopab  4983  epelg  5030  elvvuni  5179  posn  5187  frsn  5189  eqrelriv  5213  relopabiALT  5246  opabid2  5251  ididg  5275  iss  5447  ord0eln0  5779  sucidg  5803  nsuceq0  5805  onun2i  5843  funopg  5922  fn0  6011  f00  6087  f0bi  6088  f10d  6170  f1o00  6171  fo00  6172  brprcneu  6184  dffn5  6241  fsn  6402  funop  6414  funsndifnop  6416  funsneqopsn  6417  fnsnb  6432  eufnfv  6491  f1eqcocnv  6556  nfriotad  6619  riotaprop  6635  oprabid  6677  elrnmpt2  6773  ov6g  6798  ovelrn  6810  caovmo  6871  offn  6908  caofinvl  6924  fr3nr  6979  onprc  6984  ordeleqon  6988  onint0  6996  0elsuc  7035  onuninsuci  7040  orduninsuc  7043  ordzsl  7045  onzsl  7046  tfinds  7059  limomss  7070  limom  7080  peano5  7089  xpexr  7106  eqop2  7209  1stconst  7265  2ndconst  7266  funsssuppss  7321  dftpos3  7370  dftpos4  7371  wfrlem4  7418  wfrlem14  7428  oawordeulem  7634  omwordi  7651  nnmwordi  7715  riiner  7820  ecopover  7851  ecopoverOLD  7852  map0g  7897  mapsn  7899  elixpsn  7947  en0  8019  en1  8023  fiprc  8039  sbthlem2  8071  sbthlem4  8073  sbthlem5  8074  nneneq  8143  sdom1  8160  fineqvlem  8174  nfielex  8189  findcard  8199  findcard2  8200  elfiun  8336  marypha1lem  8339  oicl  8434  oif  8435  oion  8441  hartogslem1  8447  hartogs  8449  wemapso2  8458  card2on  8459  0wdom  8475  brwdom2  8478  inf3lem6  8530  cantnflem3  8588  cantnflem4  8589  wemapwe  8594  cnfcom  8597  tctr  8616  r1tr  8639  r1rankidb  8667  r1pw  8708  scottex  8748  scott0  8749  bnd2  8756  tskwe  8776  oncard  8786  cardlim  8798  harsdom  8821  en2eleq  8831  dfac8alem  8852  cardaleph  8912  iunfictbso  8937  infmap2  9040  ackbij1lem18  9059  cff  9070  cfsuc  9079  cff1  9080  cflim2  9085  cfss  9087  sdom2en01  9124  infpssrlem4  9128  fin23lem7  9138  fin23lem11  9139  isfin2-2  9141  fin23lem26  9147  fin23lem19  9158  fin23lem17  9160  isf34lem2  9195  isf34lem4  9199  fin1a2lem6  9227  fin1a2lem10  9231  fin1a2lem12  9233  itunifn  9239  hsmexlem1  9248  axcc2lem  9258  dcomex  9269  axdc3lem4  9275  ondomon  9385  konigthlem  9390  pwcfsdom  9405  cfpwsdom  9406  axpowndlem3  9421  canth4  9469  canthnumlem  9470  canthwelem  9472  canthwe  9473  canthp1lem2  9475  pwfseqlem4  9484  pwfseqlem5  9485  gchaleph  9493  gch2  9497  winainflem  9515  0tsk  9577  rankcf  9599  tskcard  9603  gruina  9640  grutsk  9644  tskmid  9662  indpi  9729  nqereu  9751  mulcanenq  9782  recmulnq  9786  archnq  9802  ltsopr  9854  1ne0sr  9917  0idsr  9918  00sr  9920  leid  10133  lelttric  10144  divcan3  10711  lemul1a  10877  nn1suc  11041  nn0n0n1ge2b  11359  xnn0xr  11368  xnn0nemnf  11374  nn0lt10b  11439  nn0ind-raph  11477  elnn1uz2  11765  indstr2  11767  uzsupss  11780  rpnnen1lem4  11817  rpnnen1lem5  11818  rpnnen1lem4OLD  11823  rpnnen1lem5OLD  11824  xrnemnf  11951  xrnepnf  11952  mnfltxr  11961  xnn0n0n1ge2b  11965  nn0pnfge0OLD  11968  xrlttri  11972  xrlttr  11973  xrleid  11983  qbtwnxr  12031  xmullem2  12095  xlemul1a  12118  xrub  12142  reltxrnmnf  12172  ixxun  12191  xnn0xrge0  12325  fztpval  12402  fseq1p1m1  12414  elfznelfzob  12574  ltweuz  12760  fzfi  12771  fsuppmapnn0fiubex  12792  ser0f  12854  0exp  12895  faclbnd4lem1  13080  bcn1  13100  hashnemnf  13132  hashv01gt1  13133  hashsnle1  13205  hashgt12el2  13211  hashmap  13222  hashpw  13223  hashf1  13241  fz1isolem  13245  hash2prb  13254  wrdlndm  13321  0wrd0  13331  wrdlen1  13343  ccatvalfn  13365  wrdl1exs1  13393  swrdlen  13423  swrdspsleq  13449  cats1un  13475  wrdind  13476  wrd2ind  13477  swrdccatin1  13483  repswsymballbi  13527  cshw1  13568  scshwfzeqfzo  13572  wrdl2exs2  13690  trclfvcotr  13750  relexp1g  13766  relexp0rel  13777  relexprelg  13778  sqr0lem  13981  sqrtsq  14010  mptfzshft  14510  fsumrev  14511  prodf1f  14624  fprodrev  14707  egt2lt3  14934  0dvds  15002  nn0o  15099  divalgmod  15129  flodddiv4  15137  bitsp1o  15155  gcddvds  15225  bezout  15260  lcmdvds  15321  rpdvds  15374  1nprm  15392  prmind2  15398  nnoddn2prmb  15518  pcpre1  15547  vdwapf  15676  vdwapid1  15679  ram0  15726  ramz  15729  prmolefac  15750  cshws0  15808  prmlem0  15812  strle1  15973  restsspw  16092  prdsdsfn  16125  imasdsfn  16174  imasaddfnlem  16188  imasvscafn  16197  xpscfv  16222  xpsfrnel  16223  isacs1i  16318  cidfn  16340  fnhomeqhomf  16351  comffn  16365  isoval  16425  sscres  16483  cofucl  16548  idffth  16593  ressffth  16598  catcoppccl  16758  estrchomfn  16775  funcestrcsetclem4  16783  funcestrcsetclem7  16786  equivestrcsetc  16792  funcsetcestrclem4  16798  funcsetcestrclem7  16801  1stfcl  16837  2ndfcl  16838  prfcl  16843  evlfcl  16862  curf1cl  16868  curfcl  16872  hofcl  16899  yonedainv  16921  pospo  16973  lubfun  16980  glbfun  16993  joindmss  17007  meetdmss  17021  ipopos  17160  acsficl2d  17176  dirref  17235  mgmidcl  17265  mgmlrid  17266  cntzssv  17761  symggrp  17820  symgid  17821  idresperm  17829  pmtrfmvdn0  17882  symggen  17890  psgnunilem1  17913  psgnprfval  17941  slwpgp  18028  frgpmhm  18178  frgpuptinv  18184  frgpup3lem  18190  gsumzoppg  18344  gsumcom2  18374  abv0  18831  rrgsupp  19291  psrvscafval  19390  psrridm  19404  ltbwe  19472  psrbag0  19494  psrbagsn  19495  subrgascl  19498  zrhrhm  19860  psgnodpmr  19936  frlmphl  20120  ellspd  20141  mattpostpos  20260  mavmul0  20358  mavmul0g  20359  mdet0f1o  20399  m1detdiag  20403  m2detleiblem5  20431  m2detleiblem6  20432  m2detleiblem3  20435  m2detleiblem4  20436  maducoeval2  20446  d1mat2pmat  20544  chpmat1dlem  20640  chpmat1d  20641  baspartn  20758  eltg3  20766  topnex  20800  fctop  20808  cctop  20810  discld  20893  mretopd  20896  neipeltop  20933  neitr  20984  restcls  20985  ordtbaslem  20992  ordtuni  20994  idcn  21061  cnrmi  21164  cmpsublem  21202  cmpsub  21203  tgcmp  21204  uncmp  21206  hauscmplem  21209  cmpfi  21211  bwth  21213  1stcrestlem  21255  disllycmp  21301  dis1stc  21302  refref  21316  kgeni  21340  1stckgenlem  21356  kqffn  21528  snfil  21668  filconn  21687  cfinfil  21697  ufileu  21723  filufint  21724  fixufil  21726  cfinufil  21732  ufilen  21734  fin1aufil  21736  fmf  21749  rnelfm  21757  flimclslem  21788  hauspwpwf1  21791  supnfcls  21824  flimfnfcls  21832  fclscmp  21834  alexsubALTlem2  21852  alexsubALTlem3  21853  alexsubALT  21855  ptcmplem1  21856  cnextrel  21867  tsmsfbas  21931  ustref  22022  trust  22033  restutop  22041  isusp  22065  xmet0  22147  imasdsf1olem  22178  blfvalps  22188  blfps  22211  blf  22212  restmetu  22375  dscmet  22377  isngp2  22401  nm0  22433  nrginvrcn  22496  nmoix  22533  qdensere  22573  iccconn  22633  iccpnfcnv  22743  xrhmeo  22745  lebnumlem3  22762  cmetss  23113  bcthlem5  23125  rrxmfval  23189  minveclem3b  23199  cniccbdd  23230  ovolicc2lem4  23288  iunmbl  23321  ioorinv  23344  ioorcl  23345  i1f1lem  23456  limcvallem  23635  ellimc2  23641  limccnp  23655  limccnp2  23656  limcco  23657  perfdvf  23667  recnprss  23668  fncpn  23696  dvcmulf  23708  c1lip1  23760  lhop2  23778  q1pcl  23915  r1pdeglt  23918  ply1remlem  23922  plyssc  23956  ulm0  24145  cxpeq0  24424  cxplea  24442  cxplogb  24524  asinlem  24595  isppw2  24841  muval2  24860  dchrfi  24980  dchrpt  24992  bposlem6  25014  lgsdir2lem2  25051  lgsqr  25076  gausslemma2dlem4  25094  2lgslem2  25120  2lgslem3  25129  2lgs  25132  2sqlem7  25149  2sqlem11  25154  chtppilim  25164  tgldimor  25397  tgcgr4  25426  tglnfn  25442  tglnunirn  25443  mirne  25562  mircinv  25563  perpln1  25605  perpln2  25606  lmiisolem  25688  xmstrkgc  25766  axcgrtr  25795  axsegconlem9  25805  axlowdimlem5  25826  axlowdimlem17  25838  axlowdim1  25839  uhgr0e  25966  edglnl  26038  uhgr0edgfi  26132  issubgr2  26164  subgrprop2  26166  egrsubgr  26169  0grsubgr  26170  0uhgrsubgr  26171  uhgrsubgrself  26172  nbgr0vtx  26252  nbgr1vtx  26254  nb3grprlem1  26282  uvtxa0  26294  uvtxa01vtx0  26297  cplgr1vlem  26325  cplgr1v  26326  usgrexilem  26336  wlkcomp  26526  wlk1walk  26535  wlkp1lem5  26574  uhgrwkspthlem1  26649  pthdlem1  26662  clwlkcomp  26675  lfgrn1cycl  26697  uspgrn2crct  26700  wwlksn0s  26746  wwlksnonfi  26816  umgrwwlks2on  26850  0ewlk  26975  0spth  26987  upgr1wlkdlem2  27006  wlk2v2e  27017  upgr3v3e3cycl  27040  upgr4cycl4dv4e  27045  eupth0  27074  frgr0v  27125  frgr1v  27135  1vwmgr  27140  ex-opab  27289  grpoinvf  27386  nvmid  27514  nmlnoubi  27651  hiidrcl  27952  hsn0elch  28105  shjshseli  28352  cmbr4i  28460  dfiop2  28612  kbpj  28815  nmopun  28873  adjeq0  28950  kbass2  28976  pjssdif1i  29034  pjinvari  29050  pjcmul2i  29061  pj3i  29067  stge1i  29097  stle0i  29098  sumdmdlem2  29278  dmdbr6ati  29282  dmdbr7ati  29283  rabsnel  29341  disjdifprg  29388  ofoprabco  29464  padct  29497  fpwrelmapffslem  29507  xrlelttric  29517  iundisj2cnt  29558  f1ocnt  29559  fz1nnct  29560  fz1nntr  29561  nn0min  29567  xrge0tsmsbi  29786  locfinref  29908  dispcmp  29926  pstmxmet  29940  xrge0iifcnv  29979  xrge0iif1  29984  qqhre  30064  esumcl  30092  esumpr2  30129  esumpinfval  30135  esumpcvgval  30140  ofcfn  30162  pwsiga  30193  prsiga  30194  sigainb  30199  ldgenpisyslem1  30226  measiuns  30280  relfae  30310  pmeasmono  30386  sitgf  30409  eulerpartgbij  30434  sgnmulsgn  30611  sgnmulsgp  30612  signswch  30638  signslema  30639  signstlen  30644  circlevma  30720  bnj145OLD  30795  bnj216  30800  bnj151  30947  bnj517  30955  bnj970  31017  bnj1145  31061  bnj1498  31129  subfacp1lem5  31166  erdszelem8  31180  kur14lem1  31188  indispconn  31216  cvmsss2  31256  msubrn  31426  dfpo2  31645  dfon2lem7  31694  frrlem6  31789  nosgnn0i  31812  nolesgn2ores  31825  nosepnelem  31830  nosepdmlem  31833  nosupbnd1lem3  31856  nosupbnd1lem5  31858  nosupbnd2lem1  31861  brbigcup  32005  elsingles  32025  fnimage  32036  funpartlem  32049  dfrdg4  32058  imagesset  32060  altopthsn  32068  elaltxp  32082  ellines  32259  linethru  32260  rankeq1o  32278  elhf2  32282  hfninf  32293  nn0prpwlem  32317  fneref  32345  neibastop2lem  32355  limsucncmpi  32444  bj-speiv  32724  bj-exlimmpbir  32907  bj-snglex  32961  bj-restpw  33045  bj-inftyexpidisj  33097  topdifinffinlem  33195  relowlssretop  33211  rdgeqoa  33218  finxpreclem6  33233  poimirlem23  33432  poimirlem29  33438  poimirlem31  33440  volsupnfl  33454  cnambfre  33458  dvasin  33496  dvacos  33497  sdclem2  33538  sstotbnd2  33573  ssbnd  33587  ismgmOLD  33649  grpokerinj  33692  rngomndo  33734  isdrngo1  33755  ac6s6  33980  iss2  34112  prtlem12  34152  riotasv2d  34243  lkrscss  34385  islshpkrN  34407  isline  35025  ispointN  35028  0psubN  35035  linepsubN  35038  atpsubN  35039  cdlemk36  36201  diafn  36323  dibfna  36443  dibvalrel  36452  dicvalrelN  36474  diclspsn  36483  dihvalrel  36568  dih1  36575  lclkrlem1  36795  lclkr  36822  mapd1o  36937  mapdin  36951  hdmapfnN  37121  hgmapfnN  37180  elrfirn  37258  ismrcd1  37261  istopclsd  37263  rabren3dioph  37379  jm2.17b  37528  jm2.22  37562  jm2.23  37563  ttac  37603  pw2f1ocnv  37604  dnnumch1  37614  hbtlem5  37698  mncn0  37709  aaitgo  37732  rngunsnply  37743  clcnvlem  37930  relexp01min  38005  ntrf  38421  ssrecnpr  38507  seff  38508  sblpnf  38509  nzss  38516  dvconstbi  38533  ipo0  38653  ifr0  38654  addrfn  38676  subrfn  38677  mulvfn  38678  refsum2cnlem1  39196  tpid2g  39316  tpid1g  39322  mapsnd  39388  ellimciota  39846  dvmptconst  40129  dvmptidg  40131  dvmulcncf  40140  dvdivcncf  40142  stoweidlem26  40243  stoweidlem50  40267  stoweidlem57  40274  funop1  41302  fun2dmnopgexmpl  41303  2ffzoeq  41338  iccpartiltu  41358  iccpartigtl  41359  zofldiv2ALTV  41574  evenprm2  41623  stgoldbwt  41664  nnsum3primesle9  41682  nnsum4primeseven  41688  nnsum4primesevenALTV  41689  tgblthelfgott  41703  tgblthelfgottOLD  41709  uspgrex  41758  0mgm  41774  nnsgrpmgm  41816  c0snmhm  41915  rngchomffvalALTV  41995  funcringcsetcALTV2lem4  42039  funcringcsetclem4ALTV  42062  srhmsubc  42076  rhmsubclem1  42086  srhmsubcALTV  42094  rhmsubcALTVlem1  42104  mapsnop  42123  zlmodzxzldeplem4  42292  zofldiv2  42325  fdivval  42333  nnlog2ge0lt1  42360  dig1  42402