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

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 𝜒
mpbiri.maj (𝜑 → (𝜓𝜒))
Assertion
Ref Expression
mpbiri (𝜑𝜓)

Proof of Theorem mpbiri
StepHypRef Expression
1 mpbiri.min . . 3 𝜒
21a1i 11 . 2 (𝜑𝜒)
3 mpbiri.maj . 2 (𝜑 → (𝜓𝜒))
42, 3mpbird 247 1 (𝜑𝜓)
Colors of variables: wff setvar class
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  1030  dedtOLD  1033  spei  2259  nfald2  2329  nfabd2  2781  raleleqALT  3152  dedhb  3370  sbceqal  3481  ssdifeq0  4042  r19.2zb  4052  dedth  4130  pwidg  4164  elpr2  4190  elpr2OLD  4191  snidg  4197  exsnrex  4212  ifpr  4224  rabrsn  4250  prid1g  4286  tpid3g  4296  pwpw0  4335  sssn  4349  preqr1OLD  4371  elpreqpr  4387  pwsnALT  4420  unimax  4464  intmin3  4496  syl6eqbr  4683  intabs  4816  pwnss  4821  0inp0  4828  copsexg  4946  euotd  4965  elopab  4973  epelg  5020  elvvuni  5169  posn  5177  frsn  5179  eqrelriv  5203  relopabiALT  5235  opabid2  5240  ididg  5264  iss  5435  ord0eln0  5767  sucidg  5791  nsuceq0  5793  onun2i  5831  funopg  5910  fn0  5998  f00  6074  f0bi  6075  f10d  6157  f1o00  6158  fo00  6159  brprcneu  6171  dffn5  6228  fsn  6387  funop  6399  funsndifnop  6401  funsneqopsn  6402  fnsnb  6417  eufnfv  6476  f1eqcocnv  6541  nfriotad  6604  riotaprop  6620  oprabid  6662  elrnmpt2  6758  ov6g  6783  ovelrn  6795  caovmo  6856  offn  6893  caofinvl  6909  fr3nr  6964  onprc  6969  ordeleqon  6973  onint0  6981  0elsuc  7020  onuninsuci  7025  orduninsuc  7028  ordzsl  7030  onzsl  7031  tfinds  7044  limomss  7055  limom  7065  peano5  7074  xpexr  7091  eqop2  7194  1stconst  7250  2ndconst  7251  funsssuppss  7306  dftpos3  7355  dftpos4  7356  wfrlem4  7403  wfrlem14  7413  oawordeulem  7619  omwordi  7636  nnmwordi  7700  riiner  7805  ecopover  7836  ecopoverOLD  7837  map0g  7882  mapsn  7884  elixpsn  7932  en0  8004  en1  8008  fiprc  8024  sbthlem2  8056  sbthlem4  8058  sbthlem5  8059  nneneq  8128  sdom1  8145  fineqvlem  8159  nfielex  8174  findcard  8184  findcard2  8185  elfiun  8321  marypha1lem  8324  oicl  8419  oif  8420  oion  8426  hartogslem1  8432  hartogs  8434  wemapso2  8443  card2on  8444  0wdom  8460  brwdom2  8463  inf3lem6  8515  cantnflem3  8573  cantnflem4  8574  wemapwe  8579  cnfcom  8582  tctr  8601  r1tr  8624  r1rankidb  8652  r1pw  8693  scottex  8733  scott0  8734  bnd2  8741  tskwe  8761  oncard  8771  cardlim  8783  harsdom  8806  en2eleq  8816  dfac8alem  8837  cardaleph  8897  iunfictbso  8922  infmap2  9025  ackbij1lem18  9044  cff  9055  cfsuc  9064  cff1  9065  cflim2  9070  cfss  9072  sdom2en01  9109  infpssrlem4  9113  fin23lem7  9123  fin23lem11  9124  isfin2-2  9126  fin23lem26  9132  fin23lem19  9143  fin23lem17  9145  isf34lem2  9180  isf34lem4  9184  fin1a2lem6  9212  fin1a2lem10  9216  fin1a2lem12  9218  itunifn  9224  hsmexlem1  9233  axcc2lem  9243  dcomex  9254  axdc3lem4  9260  ondomon  9370  konigthlem  9375  pwcfsdom  9390  cfpwsdom  9391  axpowndlem3  9406  canth4  9454  canthnumlem  9455  canthwelem  9457  canthwe  9458  canthp1lem2  9460  pwfseqlem4  9469  pwfseqlem5  9470  gchaleph  9478  gch2  9482  winainflem  9500  0tsk  9562  rankcf  9584  tskcard  9588  gruina  9625  grutsk  9629  tskmid  9647  indpi  9714  nqereu  9736  mulcanenq  9767  recmulnq  9771  archnq  9787  ltsopr  9839  1ne0sr  9902  0idsr  9903  00sr  9905  leid  10118  lelttric  10129  divcan3  10696  lemul1a  10862  nn1suc  11026  nn0n0n1ge2b  11344  xnn0xr  11353  xnn0nemnf  11359  nn0lt10b  11424  nn0ind-raph  11462  elnn1uz2  11750  indstr2  11752  uzsupss  11765  rpnnen1lem4  11802  rpnnen1lem5  11803  rpnnen1lem4OLD  11808  rpnnen1lem5OLD  11809  xrnemnf  11936  xrnepnf  11937  mnfltxr  11946  xnn0n0n1ge2b  11950  nn0pnfge0OLD  11953  xrlttri  11957  xrlttr  11958  xrleid  11968  qbtwnxr  12016  xmullem2  12080  xlemul1a  12103  xrub  12127  reltxrnmnf  12157  ixxun  12176  xnn0xrge0  12310  fztpval  12387  fseq1p1m1  12398  elfznelfzob  12558  ltweuz  12743  fzfi  12754  fsuppmapnn0fiubex  12775  ser0f  12837  0exp  12878  faclbnd4lem1  13063  bcn1  13083  hashnemnf  13115  hashv01gt1  13116  hashsnle1  13188  hashgt12el2  13194  hashmap  13205  hashpw  13206  hashf1  13224  fz1isolem  13228  hash2prb  13237  wrdlndm  13304  0wrd0  13314  wrdlen1  13326  ccatvalfn  13348  wrdl1exs1  13376  swrdlen  13405  swrdspsleq  13431  cats1un  13457  wrdind  13458  wrd2ind  13459  swrdccatin1  13464  repswsymballbi  13508  cshw1  13549  scshwfzeqfzo  13553  wrdl2exs2  13671  trclfvcotr  13731  relexp1g  13747  relexp0rel  13758  relexprelg  13759  sqr0lem  13962  sqrtsq  13991  mptfzshft  14491  fsumrev  14492  prodf1f  14605  fprodrev  14688  egt2lt3  14915  0dvds  14983  nn0o  15080  divalgmod  15110  flodddiv4  15118  bitsp1o  15136  gcddvds  15206  bezout  15241  lcmdvds  15302  rpdvds  15355  1nprm  15373  prmind2  15379  nnoddn2prmb  15499  pcpre1  15528  vdwapf  15657  vdwapid1  15660  ram0  15707  ramz  15710  prmolefac  15731  cshws0  15789  prmlem0  15793  strle1  15954  restsspw  16073  prdsdsfn  16106  imasdsfn  16155  imasaddfnlem  16169  imasvscafn  16178  xpscfv  16203  xpsfrnel  16204  isacs1i  16299  cidfn  16321  fnhomeqhomf  16332  comffn  16346  isoval  16406  sscres  16464  cofucl  16529  idffth  16574  ressffth  16579  catcoppccl  16739  estrchomfn  16756  funcestrcsetclem4  16764  funcestrcsetclem7  16767  equivestrcsetc  16773  funcsetcestrclem4  16779  funcsetcestrclem7  16782  1stfcl  16818  2ndfcl  16819  prfcl  16824  evlfcl  16843  curf1cl  16849  curfcl  16853  hofcl  16880  yonedainv  16902  pospo  16954  lubfun  16961  glbfun  16974  joindmss  16988  meetdmss  17002  ipopos  17141  acsficl2d  17157  dirref  17216  mgmidcl  17246  mgmlrid  17247  cntzssv  17742  symggrp  17801  symgid  17802  idresperm  17810  pmtrfmvdn0  17863  symggen  17871  psgnunilem1  17894  psgnprfval  17922  slwpgp  18009  frgpmhm  18159  frgpuptinv  18165  frgpup3lem  18171  gsumzoppg  18325  gsumcom2  18355  abv0  18812  rrgsupp  19272  psrvscafval  19371  psrridm  19385  ltbwe  19453  psrbag0  19475  psrbagsn  19476  subrgascl  19479  zrhrhm  19841  psgnodpmr  19917  frlmphl  20101  ellspd  20122  mattpostpos  20241  mavmul0  20339  mavmul0g  20340  mdet0f1o  20380  m1detdiag  20384  m2detleiblem5  20412  m2detleiblem6  20413  m2detleiblem3  20416  m2detleiblem4  20417  maducoeval2  20427  d1mat2pmat  20525  chpmat1dlem  20621  chpmat1d  20622  baspartn  20739  eltg3  20747  topnex  20781  fctop  20789  cctop  20791  discld  20874  mretopd  20877  neipeltop  20914  neitr  20965  restcls  20966  ordtbaslem  20973  ordtuni  20975  idcn  21042  cnrmi  21145  cmpsublem  21183  cmpsub  21184  tgcmp  21185  uncmp  21187  hauscmplem  21190  cmpfi  21192  bwth  21194  1stcrestlem  21236  disllycmp  21282  dis1stc  21283  refref  21297  kgeni  21321  1stckgenlem  21337  kqffn  21509  snfil  21649  filconn  21668  cfinfil  21678  ufileu  21704  filufint  21705  fixufil  21707  cfinufil  21713  ufilen  21715  fin1aufil  21717  fmf  21730  rnelfm  21738  flimclslem  21769  hauspwpwf1  21772  supnfcls  21805  flimfnfcls  21813  fclscmp  21815  alexsubALTlem2  21833  alexsubALTlem3  21834  alexsubALT  21836  ptcmplem1  21837  cnextrel  21848  tsmsfbas  21912  ustref  22003  trust  22014  restutop  22022  isusp  22046  xmet0  22128  imasdsf1olem  22159  blfvalps  22169  blfps  22192  blf  22193  restmetu  22356  dscmet  22358  isngp2  22382  nm0  22414  nrginvrcn  22477  nmoix  22514  qdensere  22554  iccconn  22614  iccpnfcnv  22724  xrhmeo  22726  lebnumlem3  22743  cmetss  23094  bcthlem5  23106  rrxmfval  23170  minveclem3b  23180  cniccbdd  23211  ovolicc2lem4  23269  iunmbl  23302  ioorinv  23325  ioorcl  23326  i1f1lem  23437  limcvallem  23616  ellimc2  23622  limccnp  23636  limccnp2  23637  limcco  23638  perfdvf  23648  recnprss  23649  fncpn  23677  dvcmulf  23689  c1lip1  23741  lhop2  23759  q1pcl  23896  r1pdeglt  23899  ply1remlem  23903  plyssc  23937  ulm0  24126  cxpeq0  24405  cxplea  24423  cxplogb  24505  asinlem  24576  isppw2  24822  muval2  24841  dchrfi  24961  dchrpt  24973  bposlem6  24995  lgsdir2lem2  25032  lgsqr  25057  gausslemma2dlem4  25075  2lgslem2  25101  2lgslem3  25110  2lgs  25113  2sqlem7  25130  2sqlem11  25135  chtppilim  25145  tgldimor  25378  tgcgr4  25407  tglnfn  25423  tglnunirn  25424  mirne  25543  mircinv  25544  perpln1  25586  perpln2  25587  lmiisolem  25669  xmstrkgc  25747  axcgrtr  25776  axsegconlem9  25786  axlowdimlem5  25807  axlowdimlem17  25819  axlowdim1  25820  uhgr0e  25947  edglnl  26019  uhgr0edgfi  26113  issubgr2  26145  subgrprop2  26147  egrsubgr  26150  0grsubgr  26151  0uhgrsubgr  26152  uhgrsubgrself  26153  nbgr0vtx  26233  nbgr1vtx  26235  nb3grprlem1  26263  uvtxa0  26275  uvtxa01vtx0  26278  cplgr1vlem  26306  cplgr1v  26307  usgrexilem  26317  wlkcomp  26507  wlk1walk  26516  wlkp1lem5  26555  uhgrwkspthlem1  26630  pthdlem1  26643  clwlkcomp  26656  lfgrn1cycl  26678  uspgrn2crct  26681  wwlksn0s  26727  wwlksnonfi  26797  umgrwwlks2on  26831  0ewlk  26955  0spth  26967  upgr1wlkdlem2  26986  wlk2v2e  26997  upgr3v3e3cycl  27020  upgr4cycl4dv4e  27025  eupth0  27054  frgr0v  27105  frgr1v  27115  1vwmgr  27120  frgrwopreg1  27160  frgrwopreg2  27161  ex-opab  27259  grpoinvf  27356  nvmid  27484  nmlnoubi  27621  hiidrcl  27922  hsn0elch  28075  shjshseli  28322  cmbr4i  28430  dfiop2  28582  kbpj  28785  nmopun  28843  adjeq0  28920  kbass2  28946  pjssdif1i  29004  pjinvari  29020  pjcmul2i  29031  pj3i  29037  stge1i  29067  stle0i  29068  sumdmdlem2  29248  dmdbr6ati  29252  dmdbr7ati  29253  rabsnel  29313  disjdifprg  29360  ofoprabco  29438  padct  29471  fpwrelmapffslem  29481  xrlelttric  29491  iundisj2cnt  29532  f1ocnt  29533  fz1nnct  29534  fz1nntr  29535  nn0min  29541  xrge0tsmsbi  29760  locfinref  29882  dispcmp  29900  pstmxmet  29914  xrge0iifcnv  29953  xrge0iif1  29958  qqhre  30038  esumcl  30066  esumpr2  30103  esumpinfval  30109  esumpcvgval  30114  ofcfn  30136  pwsiga  30167  prsiga  30168  sigainb  30173  ldgenpisyslem1  30200  measiuns  30254  relfae  30284  pmeasmono  30360  sitgf  30383  eulerpartgbij  30408  sgnmulsgn  30585  sgnmulsgp  30586  signswch  30612  signslema  30613  signstlen  30618  circlevma  30694  bnj145OLD  30769  bnj216  30774  bnj151  30921  bnj517  30929  bnj970  30991  bnj1145  31035  bnj1498  31103  subfacp1lem5  31140  erdszelem8  31154  kur14lem1  31162  indispconn  31190  cvmsss2  31230  msubrn  31400  dfpo2  31620  dfon2lem7  31668  frrlem6  31763  nosgnn0i  31786  nolesgn2ores  31799  nosepnelem  31804  nosepdmlem  31807  nosupbnd1lem3  31830  nosupbnd1lem5  31832  nosupbnd2lem1  31835  brbigcup  31980  elsingles  32000  fnimage  32011  funpartlem  32024  dfrdg4  32033  imagesset  32035  altopthsn  32043  elaltxp  32057  ellines  32234  linethru  32235  rankeq1o  32253  elhf2  32257  hfninf  32268  nn0prpwlem  32292  fneref  32320  neibastop2lem  32330  limsucncmpi  32419  bj-speiv  32699  bj-exlimmpbir  32882  bj-snglex  32936  bj-restpw  33020  bj-inftyexpidisj  33068  topdifinffinlem  33166  relowlssretop  33182  rdgeqoa  33189  finxpreclem6  33204  poimirlem23  33403  poimirlem29  33409  poimirlem31  33411  volsupnfl  33425  cnambfre  33429  dvasin  33467  dvacos  33468  sdclem2  33509  sstotbnd2  33544  ssbnd  33558  ismgmOLD  33620  grpokerinj  33663  rngomndo  33705  isdrngo1  33726  ac6s6  33951  prtlem12  33971  riotasv2d  34062  lkrscss  34204  islshpkrN  34226  isline  34844  ispointN  34847  0psubN  34854  linepsubN  34857  atpsubN  34858  cdlemk36  36020  diafn  36142  dibfna  36262  dibvalrel  36271  dicvalrelN  36293  diclspsn  36302  dihvalrel  36387  dih1  36394  lclkrlem1  36614  lclkr  36641  mapd1o  36756  mapdin  36770  hdmapfnN  36940  hgmapfnN  36999  elrfirn  37077  ismrcd1  37080  istopclsd  37082  rabren3dioph  37198  jm2.17b  37347  jm2.22  37381  jm2.23  37382  ttac  37422  pw2f1ocnv  37423  dnnumch1  37433  hbtlem5  37517  mncn0  37528  aaitgo  37551  rngunsnply  37562  clcnvlem  37749  relexp01min  37824  ntrf  38241  ssrecnpr  38327  seff  38328  sblpnf  38329  nzss  38336  dvconstbi  38353  ipo0  38473  ifr0  38474  addrfn  38496  subrfn  38497  mulvfn  38498  refsum2cnlem1  39016  tpid2g  39136  tpid1g  39142  mapsnd  39204  ellimciota  39646  dvmptconst  39892  dvmptidg  39894  dvmulcncf  39903  dvdivcncf  39905  stoweidlem26  40006  stoweidlem50  40030  stoweidlem57  40037  funop1  41065  fun2dmnopgexmpl  41066  2ffzoeq  41101  iccpartiltu  41122  iccpartigtl  41123  zofldiv2ALTV  41339  evenprm2  41388  stgoldbwt  41429  nnsum3primesle9  41447  nnsum4primeseven  41453  nnsum4primesevenALTV  41454  tgblthelfgott  41468  tgblthelfgottOLD  41474  uspgrex  41523  0mgm  41539  nnsgrpmgm  41581  c0snmhm  41680  rngchomffvalALTV  41760  funcringcsetcALTV2lem4  41804  funcringcsetclem4ALTV  41827  srhmsubc  41841  rhmsubclem1  41851  srhmsubcALTV  41859  rhmsubcALTVlem1  41869  mapsnop  41888  zlmodzxzldeplem4  42057  zofldiv2  42090  fdivval  42098  nnlog2ge0lt1  42125  dig1  42167
  Copyright terms: Public domain W3C validator