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

Theorem mpbiri 236
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 235 1  |-  ( ph  ->  ps )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 187
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 188
This theorem is referenced by:  dedt  965  spei  2065  nfald2  2126  nfabd2  2603  dedhb  3238  sbceqal  3348  ssdifeq0  3875  r19.2zb  3884  dedth  3957  pwidg  3989  elpr2  4012  snidg  4019  exsnrex  4031  ifpr  4042  rabrsn  4064  prid1g  4100  pwpw0  4142  sssn  4152  preqr1  4168  pwsnALT  4208  unimax  4248  intmin3  4278  syl6eqbr  4454  intabs  4577  pwnss  4581  0inp0  4588  copsexg  4698  euotd  4713  elopab  4720  epelg  4757  elvvuni  4906  posn  4914  frsn  4916  eqrelriv  4939  relopabi  4970  opabid2  4975  ididg  4999  iss  5163  ord0eln0  5487  sucidg  5511  nsuceq0  5513  onun2i  5548  funopg  5624  fn0  5704  f00  5773  f0bi  5774  f1o00  5854  fo00  5855  brprcneu  5865  dffn5  5917  fsn  6067  fnsnb  6089  fconstfvOLD  6133  eufnfv  6145  f1eqcocnv  6205  nfriotad  6266  riotaprop  6281  oprabid  6323  elrnmpt2  6414  ov6g  6439  ovelrn  6450  caovmo  6511  offn  6547  caofinvl  6563  fr3nr  6611  onprc  6616  ordeleqon  6620  onint0  6628  0elsuc  6667  onuninsuci  6672  orduninsuc  6675  ordzsl  6677  onzsl  6678  tfinds  6691  limomss  6702  limom  6712  peano5  6721  xpexr  6738  eqop2  6839  1stconst  6886  2ndconst  6887  funsssuppss  6943  dftpos3  6990  dftpos4  6991  wfrlem4  7038  wfrlem14  7048  oawordeulem  7254  omwordi  7271  nnmwordi  7335  riiner  7435  ecopover  7466  map0g  7510  mapsn  7512  elixpsn  7560  en0  7630  en1  7634  fiprc  7649  sbthlem2  7680  sbthlem4  7682  sbthlem5  7683  nneneq  7752  sdom1  7769  fineqvlem  7783  nfielex  7797  findcard  7807  findcard2  7808  elfiun  7941  marypha1lem  7944  oicl  8035  oif  8036  oion  8042  hartogslem1  8048  hartogs  8050  wemapso2  8059  card2on  8060  0wdom  8076  brwdom2  8079  inf3lem6  8129  cantnflem3  8186  cantnflem4  8187  wemapwe  8192  cnfcom  8195  tctr  8214  r1tr  8237  r1rankidb  8265  r1pw  8306  scottex  8346  scott0  8347  bnd2  8354  tskwe  8374  oncard  8384  cardlim  8396  harsdom  8419  en2eleq  8429  dfac8alem  8449  cardaleph  8509  iunfictbso  8534  infmap2  8637  ackbij1lem18  8656  cff  8667  cfsuc  8676  cff1  8677  cflim2  8682  cfss  8684  sdom2en01  8721  infpssrlem4  8725  fin23lem7  8735  fin23lem11  8736  isfin2-2  8738  fin23lem26  8744  fin23lem19  8755  fin23lem17  8757  isf34lem2  8792  isf34lem4  8796  fin1a2lem6  8824  fin1a2lem10  8828  fin1a2lem12  8830  itunifn  8836  hsmexlem1  8845  axcc2lem  8855  dcomex  8866  axdc3lem4  8872  ondomon  8977  konigthlem  8982  pwcfsdom  8997  cfpwsdom  8998  axpowndlem3  9013  canth4  9061  canthnumlem  9062  canthwelem  9064  canthwe  9065  canthp1lem2  9067  pwfseqlem4  9076  pwfseqlem5  9077  gchaleph  9085  gch2  9089  winainflem  9107  0tsk  9169  rankcf  9191  tskcard  9195  gruina  9232  grutsk  9236  tskmid  9254  indpi  9321  nqereu  9343  mulcanenq  9374  recmulnq  9378  archnq  9394  ltsopr  9446  1ne0sr  9509  0idsr  9510  00sr  9512  leid  9718  lelttric  9730  divcan3  10283  lemul1a  10448  nn1suc  10619  nn0n0n1ge2b  10922  nn0lt10b  10987  nn0ind-raph  11024  elnn1uz2  11224  indstr2  11226  uzsupss  11245  rpnnen1lem4  11282  rpnnen1lem5  11283  xrnemnf  11408  xrnepnf  11409  mnfltxr  11418  nn0pnfge0  11423  xrlttri  11427  xrlttr  11428  xrleid  11438  qbtwnxr  11482  xmullem2  11540  xlemul1a  11563  xrub  11586  reltxrnmnf  11621  ixxun  11640  fztpval  11844  fseq1p1m1  11855  elfznelfzob  12001  ltweuz  12161  fzfi  12171  fsuppmapnn0fiubex  12190  ser0f  12252  0exp  12293  faclbnd4lem1  12464  bcn1  12484  hashnemnf  12513  hashv01gt1  12514  hashle00  12563  hashgt12el2  12580  hashmap  12591  hashpw  12592  hashf1  12604  fz1isolem  12608  hash2prd  12616  hash2prv  12623  0wrd0  12669  wrdlen1  12681  ccatvalfn  12702  swrdlen  12753  swrdspsleq  12779  cats1un  12806  wrdind  12807  wrd2ind  12808  swrdccatin1  12813  repswsymballbi  12857  cshw1  12895  scshwfzeqfzo  12899  trclfvcotr  13041  relexp1g  13057  relexp0rel  13068  relexprelg  13069  sqr0lem  13272  sqrtsq  13301  mptfzshft  13806  fsumrev  13807  prodf1f  13915  fprodrev  13998  egt2lt3  14225  0dvds  14290  bitsp1o  14370  gcddvds  14440  bezout  14470  lcmdvds  14533  1nprm  14589  prmind2  14595  rpdvds  14636  pcpre1  14744  vdwapf  14874  vdwapid1  14877  ram0  14932  ramz  14935  prmolefac  14956  cshws0  15024  prmlem0  15029  strle1  15173  restsspw  15282  prdsdsfn  15315  imasdsfn  15364  imasaddfnlem  15378  imasvscafn  15387  xpscfv  15412  xpsfrnel  15413  isacs1i  15507  cidfn  15529  fnhomeqhomf  15540  comffn  15554  isoval  15614  sscres  15672  cofucl  15737  idffth  15782  ressffth  15787  catcoppccl  15947  estrchomfn  15964  funcestrcsetclem4  15972  funcestrcsetclem7  15975  equivestrcsetc  15981  funcsetcestrclem4  15987  funcsetcestrclem7  15990  1stfcl  16026  2ndfcl  16027  prfcl  16032  evlfcl  16051  curf1cl  16057  curfcl  16061  hofcl  16088  yonedainv  16110  pospo  16163  lubfun  16170  glbfun  16183  joindmss  16197  meetdmss  16211  ipopos  16350  acsficl2d  16366  dirref  16425  mgmidcl  16452  mgmlrid  16453  cntzssv  16926  symggrp  16985  symgid  16986  idresperm  16994  pmtrfmvdn0  17047  symggen  17055  psgnunilem1  17078  psgnprfval  17106  slwpgp  17193  frgpmhm  17343  frgpuptinv  17349  frgpup3lem  17355  gsumzoppg  17505  gsumcom2  17535  abv0  17987  rrgsupp  18443  psrvscafval  18542  psrridm  18556  ltbwe  18624  psrbag0  18645  psrbagsn  18646  subrgascl  18649  zrhrhm  19007  psgnodpmr  19082  frlmphl  19263  ellspd  19284  mattpostpos  19403  mavmul0  19501  mavmul0g  19502  mdet0f1o  19542  m1detdiag  19546  m2detleiblem5  19574  m2detleiblem6  19575  m2detleiblem3  19578  m2detleiblem4  19579  maducoeval2  19589  d1mat2pmat  19687  chpmat1dlem  19783  chpmat1d  19784  baspartn  19893  eltg3  19901  fctop  19943  cctop  19945  discld  20029  mretopd  20032  neipeltop  20069  neitr  20120  restcls  20121  ordtbaslem  20128  ordtuni  20130  idcn  20197  cnrmi  20300  cmpsublem  20338  cmpsub  20339  tgcmp  20340  uncmp  20342  hauscmplem  20345  cmpfi  20347  bwth  20349  1stcrestlem  20391  disllycmp  20437  dis1stc  20438  refref  20452  kgeni  20476  1stckgenlem  20492  kqffn  20664  snfil  20803  filcon  20822  cfinfil  20832  ufileu  20858  filufint  20859  fixufil  20861  cfinufil  20867  ufilen  20869  fin1aufil  20871  fmf  20884  rnelfm  20892  flimclslem  20923  hauspwpwf1  20926  supnfcls  20959  flimfnfcls  20967  fclscmp  20969  alexsubALTlem2  20987  alexsubALTlem3  20988  alexsubALT  20990  ptcmplem1  20991  cnextrel  21002  tsmsfbas  21066  ustref  21157  trust  21168  restutop  21176  isusp  21200  xmet0  21281  imasdsf1olem  21312  blfvalps  21322  blfps  21345  blf  21346  restmetu  21509  dscmet  21511  isngp2  21535  nm0  21564  nrginvrcn  21618  nmoix  21654  qdensere  21694  iccconn  21752  iccpnfcnv  21861  xrhmeo  21863  lebnumlem3  21880  cmetss  22170  bcthlem5  22182  rrxmfval  22246  minveclem3b  22256  cniccbdd  22286  ovolicc2lem4OLD  22347  ovolicc2lem4  22348  iunmbl  22380  ioorinv  22402  ioorcl  22403  ioorinvOLD  22407  ioorclOLD  22408  i1f1lem  22521  limcvallem  22700  ellimc2  22706  limccnp  22720  limccnp2  22721  limcco  22722  perfdvf  22732  recnprss  22733  fncpn  22761  dvcmulf  22773  c1lip1  22823  lhop2  22841  q1pcl  22978  r1pdeglt  22981  ply1remlem  22985  plyssc  23019  ulm0  23208  cxpeq0  23485  cxplea  23503  cxplogb  23585  asinlem  23656  isppw2  23902  muval2  23921  dchrfi  24043  dchrpt  24055  bposlem6  24077  lgsdir2lem2  24112  lgsqr  24134  2sqlem7  24158  2sqlem11  24163  chtppilim  24173  tgldimor  24406  tglnfn  24449  tglnunirn  24450  mircinv  24569  perpln1  24609  perpln2  24610  lmiisolem  24691  xmstrkgc  24759  axcgrtr  24788  axsegconlem9  24798  axlowdimlem5  24819  axlowdimlem17  24831  axlowdim1  24832  uhgra0  24879  uhgra0v  24880  umgra0  24895  usgra0  24940  usgra0v  24941  usgraedg4  24957  usgra1v  24960  nb3graprlem1  25021  cusgra1v  25031  cusgraexilem2  25037  uvtx01vtx  25062  wlkcomp  25095  wlkntrl  25134  0spth  25143  1pthonlem1  25161  2pthlem1  25167  usgra2wlkspthlem1  25189  3v3e3cycl1  25214  constr3trllem1  25220  constr3pthlem3  25227  4cycl4v4e  25236  4cycl4dv  25237  0conngra  25244  wwlkn0s  25275  clwlkcomp  25333  frgra0v  25563  frgra1v  25568  1vwmgra  25573  vdgfrgragt2  25597  frgrancvvdeqlem3  25602  frgrawopreg1  25620  frgrawopreg2  25621  2spot0  25634  ex-opab  25724  grpoinvf  25810  ismgmOLD  25890  rngomndo  25991  nvmid  26128  nmlnoubi  26279  hiidrcl  26580  hsn0elch  26733  shjshseli  26978  cmbr4i  27086  dfiop2  27238  kbpj  27441  nmopun  27499  adjeq0  27576  kbass2  27602  pjssdif1i  27660  pjinvari  27676  pjcmul2i  27687  pj3i  27693  stge1i  27723  stle0i  27724  sumdmdlem2  27904  dmdbr6ati  27908  dmdbr7ati  27909  rabsnel  27971  disjdifprg  28021  ofoprabco  28104  padct  28147  fpwrelmapffslem  28157  xrlelttric  28169  iundisj2cnt  28208  f1ocnt  28209  fz1nnct  28210  fz1nntr  28211  nn0min  28219  xrge0tsmsbi  28385  locfinref  28504  dispcmp  28522  pstmxmet  28536  xrge0iifcnv  28575  xrge0iif1  28580  qqhre  28660  esumcl  28687  esumpr2  28724  esumpinfval  28730  esumpcvgval  28735  ofcfn  28757  pwsiga  28788  prsiga  28789  sigainb  28794  ldgenpisyslem1  28821  measiuns  28875  relfae  28906  pmeasmono  28982  sitgf  29005  eulerpartgbij  29028  sgnmulsgn  29205  sgnmulsgp  29206  signswch  29235  signslema  29236  signstlen  29241  bnj145OLD  29320  bnj216  29325  bnj151  29473  bnj517  29481  bnj970  29543  bnj1145  29587  bnj1498  29655  subfacp1lem5  29692  erdszelem8  29706  kur14lem1  29714  indispcon  29742  cvmsss2  29782  msubrn  29952  dfpo2  30179  dfon2lem7  30219  frrlem6  30307  nosgnn0i  30330  nobndlem2  30364  nobndlem4  30366  nobndlem5  30367  nobndlem6  30368  brbigcup  30447  elsingles  30467  fnimage  30478  funpartlem  30491  dfrdg4  30500  imagesset  30502  altopthsn  30510  elaltxp  30524  ellines  30701  linethru  30702  rankeq1o  30720  elhf2  30724  hfninf  30735  nn0prpwlem  30760  fneref  30788  neibastop2lem  30798  limsucncmpi  30887  bj-dedthm  30936  bj-speiv  31062  bj-exlimmpbir  31261  bj-snglex  31313  bj-inftyexpidisj  31394  topdifinffinlem  31481  relowlssretop  31497  poimirlem23  31667  poimirlem29  31673  poimirlem31  31675  volsupnfl  31689  cnambfre  31693  dvasin  31732  dvacos  31733  sdclem2  31775  sstotbnd2  31810  ssbnd  31824  grpokerinj  31887  isdrngo1  31899  ac6s6  32119  prtlem12  32147  riotasv2d  32238  lkrscss  32373  islshpkrN  32395  isline  33013  ispointN  33016  0psubN  33023  linepsubN  33026  atpsubN  33027  cdlemk36  34189  diafn  34311  dibfna  34431  dibvalrel  34440  dicvalrelN  34462  diclspsn  34471  dihvalrel  34556  dih1  34563  lclkrlem1  34783  lclkr  34810  mapd1o  34925  mapdin  34939  hdmapfnN  35109  hgmapfnN  35168  elrfirn  35246  ismrcd1  35249  istopclsd  35251  rabren3dioph  35367  jm2.17b  35521  jm2.22  35560  jm2.23  35561  ttac  35601  pw2f1ocnv  35602  dnnumch1  35612  hbtlem5  35697  mncn0  35708  aaitgo  35731  rngunsnply  35742  relexp01min  35948  ssrecnpr  36297  seff  36298  sblpnf  36299  nzss  36307  dvconstbi  36324  ipo0  36443  ifr0  36444  addrfn  36466  subrfn  36467  mulvfn  36468  refsum2cnlem1  37002  ellimciota  37270  dvmptconst  37361  dvmptidg  37363  dvmulcncf  37373  dvdivcncf  37375  stoweidlem26  37459  stoweidlem50  37484  stoweidlem57  37491  iccpartiltu  38139  iccpartigtl  38140  zofldiv2ALTV  38194  evenprm2  38245  stgoldbwt  38280  nnsum3primesle9  38292  nnsum4primeseven  38298  nnsum4primesevenALTV  38299  tgblthelfgott  38311  2ffzoeq  38426  uhguhgra  38455  uhg0e  38459  uhgres  38462  fusgraimpcl  38510  fusgraimpclALT  38512  0mgm  38545  nnsgrpmgm  38587  c0snmhm  38686  rngchomffvalALTV  38768  funcringcsetcALTV2lem4  38812  funcringcsetclem4ALTV  38835  srhmsubc  38849  rhmsubclem1  38859  srhmsubcALTV  38868  rhmsubcALTVlem1  38878  mapsnop  38899  zlmodzxzldeplem4  39069  nn0o  39103  zofldiv2  39112  fdivval  39124  nnlog2ge0lt1  39151  dig1  39193
  Copyright terms: Public domain W3C validator