MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  mpbiri Structured version   Visualization version   Unicode version

Theorem mpbiri 241
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
StepHypRef Expression
1 mpbiri.min . . 3  |-  ch
21a1i 11 . 2  |-  ( ph  ->  ch )
3 mpbiri.maj . 2  |-  ( ph  ->  ( ps  <->  ch )
)
42, 3mpbird 240 1  |-  ( ph  ->  ps )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 189
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 190
This theorem is referenced by:  dedt  974  spei  2116  nfald2  2176  nfabd2  2622  raleleqALT  3018  dedhb  3220  sbceqal  3331  ssdifeq0  3862  r19.2zb  3871  dedth  3944  pwidg  3976  elpr2  3999  snidg  4006  exsnrex  4021  ifpr  4032  rabrsn  4055  prid1g  4091  pwpw0  4133  sssn  4143  preqr1OLD  4162  elpreqpr  4175  pwsnALT  4207  unimax  4247  intmin3  4277  syl6eqbr  4456  intabs  4581  pwnss  4585  0inp0  4592  copsexg  4704  euotd  4719  elopab  4726  epelg  4768  elvvuni  4917  posn  4925  frsn  4927  eqrelriv  4950  relopabi  4981  opabid2  4986  ididg  5010  iss  5174  ord0eln0  5500  sucidg  5524  nsuceq0  5526  onun2i  5561  funopg  5637  fn0  5721  f00  5792  f0bi  5793  f10d  5873  f1o00  5874  fo00  5875  brprcneu  5885  dffn5  5937  fsn  6090  fnsnb  6112  fconstfvOLD  6157  eufnfv  6169  f1eqcocnv  6229  nfriotad  6290  riotaprop  6305  oprabid  6347  elrnmpt2  6441  ov6g  6466  ovelrn  6477  caovmo  6538  offn  6574  caofinvl  6590  fr3nr  6638  onprc  6643  ordeleqon  6647  onint0  6655  0elsuc  6694  onuninsuci  6699  orduninsuc  6702  ordzsl  6704  onzsl  6705  tfinds  6718  limomss  6729  limom  6739  peano5  6748  xpexr  6765  eqop2  6866  1stconst  6916  2ndconst  6917  funsssuppss  6973  dftpos3  7022  dftpos4  7023  wfrlem4  7070  wfrlem14  7080  oawordeulem  7286  omwordi  7303  nnmwordi  7367  riiner  7467  ecopover  7498  map0g  7542  mapsn  7544  elixpsn  7592  en0  7663  en1  7667  fiprc  7682  sbthlem2  7714  sbthlem4  7716  sbthlem5  7717  nneneq  7786  sdom1  7803  fineqvlem  7817  nfielex  7831  findcard  7841  findcard2  7842  elfiun  7975  marypha1lem  7978  oicl  8075  oif  8076  oion  8082  hartogslem1  8088  hartogs  8090  wemapso2  8099  card2on  8100  0wdom  8116  brwdom2  8119  inf3lem6  8169  cantnflem3  8227  cantnflem4  8228  wemapwe  8233  cnfcom  8236  tctr  8255  r1tr  8278  r1rankidb  8306  r1pw  8347  scottex  8387  scott0  8388  bnd2  8395  tskwe  8415  oncard  8425  cardlim  8437  harsdom  8460  en2eleq  8470  dfac8alem  8491  cardaleph  8551  iunfictbso  8576  infmap2  8679  ackbij1lem18  8698  cff  8709  cfsuc  8718  cff1  8719  cflim2  8724  cfss  8726  sdom2en01  8763  infpssrlem4  8767  fin23lem7  8777  fin23lem11  8778  isfin2-2  8780  fin23lem26  8786  fin23lem19  8797  fin23lem17  8799  isf34lem2  8834  isf34lem4  8838  fin1a2lem6  8866  fin1a2lem10  8870  fin1a2lem12  8872  itunifn  8878  hsmexlem1  8887  axcc2lem  8897  dcomex  8908  axdc3lem4  8914  ondomon  9019  konigthlem  9024  pwcfsdom  9039  cfpwsdom  9040  axpowndlem3  9055  canth4  9103  canthnumlem  9104  canthwelem  9106  canthwe  9107  canthp1lem2  9109  pwfseqlem4  9118  pwfseqlem5  9119  gchaleph  9127  gch2  9131  winainflem  9149  0tsk  9211  rankcf  9233  tskcard  9237  gruina  9274  grutsk  9278  tskmid  9296  indpi  9363  nqereu  9385  mulcanenq  9416  recmulnq  9420  archnq  9436  ltsopr  9488  1ne0sr  9551  0idsr  9552  00sr  9554  leid  9760  lelttric  9772  divcan3  10327  lemul1a  10492  nn1suc  10663  nn0n0n1ge2b  10967  nn0lt10b  11032  nn0ind-raph  11069  elnn1uz2  11269  indstr2  11271  uzsupss  11290  rpnnen1lem4  11327  rpnnen1lem5  11328  xrnemnf  11453  xrnepnf  11454  mnfltxr  11463  nn0pnfge0  11468  xrlttri  11472  xrlttr  11473  xrleid  11483  qbtwnxr  11527  xmullem2  11585  xlemul1a  11608  xrub  11631  reltxrnmnf  11666  ixxun  11685  fztpval  11892  fseq1p1m1  11903  elfznelfzob  12052  ltweuz  12213  fzfi  12223  fsuppmapnn0fiubex  12242  ser0f  12304  0exp  12345  faclbnd4lem1  12516  bcn1  12536  hashnemnf  12565  hashv01gt1  12566  hashle00  12615  hashgt12el2  12635  hashmap  12646  hashpw  12647  hashf1  12659  fz1isolem  12663  hash2prb  12672  0wrd0  12735  wrdlen1  12747  ccatvalfn  12768  wrdl1exs1  12793  swrdlen  12822  swrdspsleq  12848  cats1un  12875  wrdind  12876  wrd2ind  12877  swrdccatin1  12882  repswsymballbi  12926  cshw1  12964  scshwfzeqfzo  12968  wrdl2exs2  13077  trclfvcotr  13128  relexp1g  13144  relexp0rel  13155  relexprelg  13156  sqr0lem  13359  sqrtsq  13388  mptfzshft  13894  fsumrev  13895  prodf1f  14003  fprodrev  14086  egt2lt3  14313  0dvds  14378  bitsp1o  14461  gcddvds  14532  bezout  14565  lcmdvds  14628  1nprm  14684  prmind2  14690  rpdvds  14731  pcpre1  14847  vdwapf  14977  vdwapid1  14980  ram0  15035  ramz  15038  prmolefac  15059  cshws0  15127  prmlem0  15132  strle1  15276  restsspw  15385  prdsdsfn  15418  imasdsfn  15470  imasdsfnOLD  15482  imasaddfnlem  15489  imasvscafn  15498  xpscfv  15523  xpsfrnel  15524  isacs1i  15618  cidfn  15640  fnhomeqhomf  15651  comffn  15665  isoval  15725  sscres  15783  cofucl  15848  idffth  15893  ressffth  15898  catcoppccl  16058  estrchomfn  16075  funcestrcsetclem4  16083  funcestrcsetclem7  16086  equivestrcsetc  16092  funcsetcestrclem4  16098  funcsetcestrclem7  16101  1stfcl  16137  2ndfcl  16138  prfcl  16143  evlfcl  16162  curf1cl  16168  curfcl  16172  hofcl  16199  yonedainv  16221  pospo  16274  lubfun  16281  glbfun  16294  joindmss  16308  meetdmss  16322  ipopos  16461  acsficl2d  16477  dirref  16536  mgmidcl  16563  mgmlrid  16564  cntzssv  17037  symggrp  17096  symgid  17097  idresperm  17105  pmtrfmvdn0  17158  symggen  17166  psgnunilem1  17189  psgnprfval  17217  slwpgp  17320  frgpmhm  17470  frgpuptinv  17476  frgpup3lem  17482  gsumzoppg  17632  gsumcom2  17662  abv0  18114  rrgsupp  18570  psrvscafval  18669  psrridm  18683  ltbwe  18751  psrbag0  18772  psrbagsn  18773  subrgascl  18776  zrhrhm  19138  psgnodpmr  19213  frlmphl  19394  ellspd  19415  mattpostpos  19534  mavmul0  19632  mavmul0g  19633  mdet0f1o  19673  m1detdiag  19677  m2detleiblem5  19705  m2detleiblem6  19706  m2detleiblem3  19709  m2detleiblem4  19710  maducoeval2  19720  d1mat2pmat  19818  chpmat1dlem  19914  chpmat1d  19915  baspartn  20024  eltg3  20032  fctop  20074  cctop  20076  discld  20160  mretopd  20163  neipeltop  20200  neitr  20251  restcls  20252  ordtbaslem  20259  ordtuni  20261  idcn  20328  cnrmi  20431  cmpsublem  20469  cmpsub  20470  tgcmp  20471  uncmp  20473  hauscmplem  20476  cmpfi  20478  bwth  20480  1stcrestlem  20522  disllycmp  20568  dis1stc  20569  refref  20583  kgeni  20607  1stckgenlem  20623  kqffn  20795  snfil  20934  filcon  20953  cfinfil  20963  ufileu  20989  filufint  20990  fixufil  20992  cfinufil  20998  ufilen  21000  fin1aufil  21002  fmf  21015  rnelfm  21023  flimclslem  21054  hauspwpwf1  21057  supnfcls  21090  flimfnfcls  21098  fclscmp  21100  alexsubALTlem2  21118  alexsubALTlem3  21119  alexsubALT  21121  ptcmplem1  21122  cnextrel  21133  tsmsfbas  21197  ustref  21288  trust  21299  restutop  21307  isusp  21331  xmet0  21412  imasdsf1olem  21443  blfvalps  21453  blfps  21476  blf  21477  restmetu  21640  dscmet  21642  isngp2  21666  nm0  21695  nrginvrcn  21749  nmoix  21789  nmoixOLD  21805  qdensere  21845  iccconn  21903  iccpnfcnv  22027  xrhmeo  22029  lebnumlem3  22046  lebnumlem3OLD  22049  cmetss  22339  bcthlem5  22351  rrxmfval  22415  minveclem3b  22425  minveclem3bOLD  22437  cniccbdd  22467  ovolicc2lem4OLD  22528  ovolicc2lem4  22529  iunmbl  22562  ioorinv  22584  ioorcl  22585  ioorinvOLD  22589  ioorclOLD  22590  i1f1lem  22703  limcvallem  22882  ellimc2  22888  limccnp  22902  limccnp2  22903  limcco  22904  perfdvf  22914  recnprss  22915  fncpn  22943  dvcmulf  22955  c1lip1  23005  lhop2  23023  q1pcl  23162  r1pdeglt  23165  ply1remlem  23169  plyssc  23210  ulm0  23402  cxpeq0  23679  cxplea  23697  cxplogb  23779  asinlem  23850  isppw2  24098  muval2  24117  dchrfi  24239  dchrpt  24251  bposlem6  24273  lgsdir2lem2  24308  lgsqr  24330  2sqlem7  24354  2sqlem11  24359  chtppilim  24369  tgldimor  24602  tgcgr4  24632  tglnfn  24648  tglnunirn  24649  mirne  24768  mircinv  24769  perpln1  24811  perpln2  24812  lmiisolem  24894  xmstrkgc  24972  axcgrtr  25001  axsegconlem9  25011  axlowdimlem5  25032  axlowdimlem17  25044  axlowdim1  25045  uhgra0  25092  uhgra0v  25093  umgra0  25108  usgra0v  25154  usgraedg4  25170  usgra1v  25173  usgraexmpl  25185  nb3graprlem1  25235  cusgra1v  25245  cusgraexilem2  25251  uvtx01vtx  25276  wlkcomp  25309  wlkntrl  25348  0spth  25357  1pthonlem1  25375  2pthlem1  25381  usgra2wlkspthlem1  25403  3v3e3cycl1  25428  constr3trllem1  25434  constr3pthlem3  25441  4cycl4v4e  25450  4cycl4dv  25451  0conngra  25458  wwlkn0s  25489  clwlkcomp  25547  frgra0v  25777  frgra1v  25782  1vwmgra  25787  vdgfrgragt2  25811  frgrancvvdeqlem3  25816  frgrawopreg1  25834  frgrawopreg2  25835  2spot0  25848  ex-opab  25938  grpoinvf  26024  ismgmOLD  26104  rngomndo  26205  nvmid  26342  nmlnoubi  26493  hiidrcl  26804  hsn0elch  26957  shjshseli  27202  cmbr4i  27310  dfiop2  27462  kbpj  27665  nmopun  27723  adjeq0  27800  kbass2  27826  pjssdif1i  27884  pjinvari  27900  pjcmul2i  27911  pj3i  27917  stge1i  27947  stle0i  27948  sumdmdlem2  28128  dmdbr6ati  28132  dmdbr7ati  28133  rabsnel  28194  disjdifprg  28239  ofoprabco  28319  padct  28359  fpwrelmapffslem  28369  xrlelttric  28381  iundisj2cnt  28427  f1ocnt  28428  fz1nnct  28429  fz1nntr  28430  nn0min  28436  xrge0tsmsbi  28600  locfinref  28719  dispcmp  28737  pstmxmet  28751  xrge0iifcnv  28790  xrge0iif1  28795  qqhre  28875  esumcl  28902  esumpr2  28939  esumpinfval  28945  esumpcvgval  28950  ofcfn  28972  pwsiga  29003  prsiga  29004  sigainb  29009  ldgenpisyslem1  29036  measiuns  29090  relfae  29120  pmeasmono  29207  sitgf  29230  eulerpartgbij  29255  sgnmulsgn  29470  sgnmulsgp  29471  signswch  29500  signslema  29501  signstlen  29506  bnj145OLD  29585  bnj216  29590  bnj151  29738  bnj517  29746  bnj970  29808  bnj1145  29852  bnj1498  29920  subfacp1lem5  29957  erdszelem8  29971  kur14lem1  29979  indispcon  30007  cvmsss2  30047  msubrn  30217  dfpo2  30445  dfon2lem7  30485  frrlem6  30573  nosgnn0i  30596  nobndlem2  30632  nobndlem4  30634  nobndlem5  30635  nobndlem6  30636  brbigcup  30715  elsingles  30735  fnimage  30746  funpartlem  30759  dfrdg4  30768  imagesset  30770  altopthsn  30778  elaltxp  30792  ellines  30969  linethru  30970  rankeq1o  30988  elhf2  30992  hfninf  31003  nn0prpwlem  31028  fneref  31056  neibastop2lem  31066  limsucncmpi  31155  bj-dedthm  31200  bj-speiv  31371  bj-exlimmpbir  31560  bj-snglex  31613  bj-inftyexpidisj  31698  topdifinffinlem  31796  relowlssretop  31812  rdgeqoa  31819  finxpreclem6  31834  poimirlem23  32009  poimirlem29  32015  poimirlem31  32017  volsupnfl  32031  cnambfre  32035  dvasin  32074  dvacos  32075  sdclem2  32117  sstotbnd2  32152  ssbnd  32166  grpokerinj  32229  isdrngo1  32241  ac6s6  32461  prtlem12  32485  riotasv2d  32575  lkrscss  32710  islshpkrN  32732  isline  33350  ispointN  33353  0psubN  33360  linepsubN  33363  atpsubN  33364  cdlemk36  34526  diafn  34648  dibfna  34768  dibvalrel  34777  dicvalrelN  34799  diclspsn  34808  dihvalrel  34893  dih1  34900  lclkrlem1  35120  lclkr  35147  mapd1o  35262  mapdin  35276  hdmapfnN  35446  hgmapfnN  35505  elrfirn  35583  ismrcd1  35586  istopclsd  35588  rabren3dioph  35704  jm2.17b  35857  jm2.22  35896  jm2.23  35897  ttac  35937  pw2f1ocnv  35938  dnnumch1  35948  hbtlem5  36033  mncn0  36044  aaitgo  36074  rngunsnply  36085  clcnvlem  36276  relexp01min  36351  ssrecnpr  36701  seff  36702  sblpnf  36703  nzss  36711  dvconstbi  36728  ipo0  36847  ifr0  36848  addrfn  36870  subrfn  36871  mulvfn  36872  refsum2cnlem1  37399  mapsnd  37530  ellimciota  37780  dvmptconst  37871  dvmptidg  37873  dvmulcncf  37883  dvdivcncf  37885  stoweidlem26  37987  stoweidlem50  38012  stoweidlem57  38019  iccpartiltu  38871  iccpartigtl  38872  zofldiv2ALTV  38926  evenprm2  38977  stgoldbwt  39012  nnsum3primesle9  39024  nnsum4primeseven  39030  nnsum4primesevenALTV  39031  tgblthelfgott  39043  funop  39157  funop1  39158  funsndifnop  39160  funsneqopsn  39161  fun2dmnopgexmpl  39166  2ffzoeq  39202  xnn0xr  39217  xnn0xrge0  39218  xnn0nemnf  39224  uhgruhgra  39303  uhgr0e  39307  usgr1vr  39475  issubgr2  39490  subgrprop2  39492  egrsubgr  39495  0grsubgr  39496  0uhgrsubgr  39497  uhgrsubgrself  39498  nbgr0vtx  39570  nbgr1vtx  39572  nb3grprlem1  39600  uvtxa0  39612  uvtxa01vtx0  39615  cplgr0v  39641  usgrexi  39652  1wlkvtxiedg  39783  rel1wlk  39785  1wlkcomp  39788  1wlk1walk  39793  uhgr1wlkspthlem1  39881  pthdlem1  39888  clWlkcomp  39901  lfgrn1cycl  39920  uspgrn2crct  39922  0ewlk  39924  is01wlk  39930  is0Trl  39935  0spth-av  39938  upgr11wlkdlem2  39957  1wlk2v2e  39968  upgr3v3e3cycl  40017  upgr4cycl4dv4e  40022  0vconngr  40030  uhguhgra  40053  uhg0e  40057  uhgres  40060  fusgraimpcl  40108  fusgraimpclALT  40110  0mgm  40143  nnsgrpmgm  40185  c0snmhm  40284  rngchomffvalALTV  40366  funcringcsetcALTV2lem4  40410  funcringcsetclem4ALTV  40433  srhmsubc  40447  rhmsubclem1  40457  srhmsubcALTV  40466  rhmsubcALTVlem1  40476  mapsnop  40495  zlmodzxzldeplem4  40665  nn0o  40698  zofldiv2  40707  fdivval  40719  nnlog2ge0lt1  40746  dig1  40788
  Copyright terms: Public domain W3C validator