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

Theorem mpbir 232
Description: An inference from a biconditional, related to modus ponens. (Contributed by NM, 28-Dec-1992.)
Hypotheses
Ref Expression
mpbir.min 𝜓
mpbir.maj (𝜑𝜓)
Assertion
Ref Expression
mpbir 𝜑

Proof of Theorem mpbir
StepHypRef Expression
1 mpbir.min . 2 𝜓
2 mpbir.maj . . 3 (𝜑𝜓)
32biimpri 229 . 2 (𝜓𝜑)
41, 3ax-mp 5 1 𝜑
Colors of variables: wff setvar class
Syntax hints:  wb 207
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 208
This theorem is referenced by:  pm5.74ri  273  con4bii  322  imnani  401  mpbir2an  707  biadanOLD  816  imorri  851  orri  858  mpbir3an  1335  xorexmid  1513  tru  1534  had1  1597  nic-mpALT  1666  nic-ax  1667  nic-axALT  1668  nfi  1782  mpgbir  1793  nfxfr  1846  19.35ri  1873  ax5e  1906  ax6ev  1965  sbt  2064  equsb1v  2105  ax13  2388  ax13ALT  2444  euequOLD  2682  moanmo  2706  axi12  2794  axi12OLD  2795  axbnd  2796  axexte  2799  axextmo  2802  nulmo  2803  vexw  2810  eqeltri  2914  nfcxfr  2980  neir  3024  neirr  3030  eqnetri  3091  nelir  3131  mprgbir  3158  cbvrexdva2  3463  vexOLD  3504  issetri  3516  moeq  3702  rmoeq  3733  cdeqi  3760  eqsstri  4005  3sstr4i  4014  rmo0  4323  rabnc  4345  reuprg  4638  tpid1  4703  tpid2  4705  mosneq  4772  pwv  4834  uni0  4864  int0  4888  eqbrtri  5084  tr0  5180  trv  5181  zfrep4  5197  axnulALT  5205  0ex  5208  inex1  5218  elpwi2  5246  0elpw  5253  axpow2  5265  axpow3  5266  dvdemo1  5271  vpwex  5275  zfpair2  5327  exss  5352  brv  5361  opwo0id  5384  moop2  5389  pwundifOLD  5456  0sn0ep  5469  po0  5489  epse  5537  relxp  5572  rel0  5671  relopabiv  5692  relopabi  5693  relopabiALT  5694  eliunxp  5707  opeliunxp2  5708  dmi  5790  dmep  5792  domepOLD  5793  xpidtr  5981  xpima  6038  dmsn0  6065  cnvsn0  6066  0elon  6243  funmpt  6392  funmpt2  6393  funcnv0  6419  isarep2  6442  fresaunres2  6549  f0  6559  f10d  6647  f1o00  6648  f1oi  6651  f1osn  6653  brprcneu  6661  opabiotafun  6743  fvopab3ig  6763  opabex  6980  mptexgf  6982  eufnfv  6988  isof1oopb  7072  ncanth  7106  mpofun  7270  reldmmpo  7279  ovid  7285  ovidig  7286  ovidi  7287  ovig  7290  ov3  7305  caovmo  7379  relmptopab  7389  porpss  7447  uniex2  7458  tfinds2  7571  finds  7601  finds2  7603  oprabex  7673  oprabex3  7674  f1stres  7709  f2ndres  7710  relmpoopab  7785  fsplitfpar  7810  opeliunxp2f  7872  tpos0  7918  wfrrel  7956  wfrlem14  7964  wfrlem16  7966  issmo  7981  tfrlem6  8014  tfrlem8  8016  tfrlem16  8025  tfr1a  8026  tfr1  8029  tz7.44lem1  8037  seqomlem2  8083  seqomlem3  8084  seqomlem4  8085  fnseqom  8087  0lt1o  8125  0we1  8127  eqer  8319  ecopover  8396  mapsnf1o3  8453  ssdomg  8549  ensn1  8567  snfi  8588  xpcomf1o  8600  map2xp  8681  limensuci  8687  sdom1  8712  unblem4  8767  fidomdm  8795  marypha1lem  8891  hartogslem1  9000  hartogs  9002  card2on  9012  nelaneq  9057  epinid0  9058  ruALT  9061  elnanel  9064  cnvepnep  9065  inf2  9080  inf3lem6  9090  infeq5i  9093  zfinf2  9099  cantnflt  9129  cnfcom  9157  trcl  9164  tz9.1c  9166  tc2  9178  r1funlim  9189  r1fnon  9190  karden  9318  tskwe  9373  cardprclem  9402  pm54.43  9423  r0weon  9432  iunmapdisj  9443  alephfnon  9485  alephfplem4  9527  alephfp  9528  alephval3  9530  kmlem2  9571  dju1dif  9592  ackbij1  9654  ackbij2lem2  9656  ackbij2  9659  infpssrlem3  9721  hsmexlem4  9845  hsmexlem5  9846  ac2  9877  axac3  9880  ac6  9896  axdclem2  9936  dmct  9940  ondomon  9979  alephsucpw  9986  pwcfsdom  9999  cfpwsdom  10000  smobeth  10002  axpowndlem3  10015  zfcndun  10031  zfcndpow  10032  zfcndinf  10034  zfcndac  10035  wunex2  10154  uniwun  10156  wuncval2  10163  grur1  10236  axgroth5  10240  axgroth2  10241  axgroth6  10244  axgroth3  10247  grothtsk  10251  inaprc  10252  ltsopi  10304  dmaddpi  10306  dmmulpi  10307  1lt2pi  10321  nqerf  10346  addnqf  10364  mulnqf  10365  1lt2nq  10389  m1p1sr  10508  m1m1sr  10509  0lt1sr  10511  axaddf  10561  axmulf  10562  ax1cn  10565  subaddrii  10969  ixi  11263  recgt0ii  11540  nn1suc  11653  neg1lt0  11748  4d2e2  11801  arch  11888  un0mulcl  11925  pnf0xnn0  11968  3halfnz  12055  nummac  12137  indstr  12310  mnfltpnf  12516  ioof  12830  0nelfz1  12921  fzp1disj  12961  fzp1nel  12986  fzof  13030  om2uzrani  13315  om2uzf1oi  13316  uzrdglem  13320  uzrdgfni  13321  uzrdg0i  13322  ltwenn  13325  hashgf1o  13334  axdc4uzlem  13346  sq0  13550  irec  13559  facmapnn  13640  hashkf  13687  hashfxnn0  13692  hashf  13693  hash0  13723  prhash2ex  13755  hashsslei  13782  hashxplem  13789  hashbclem  13805  hashf1lem1  13808  wrdexgOLD  13867  s1dm  13957  eqs1  13961  ccat2s1p1  13980  cats1un  14078  revs1  14122  0csh0  14150  cshw1  14179  cats1fvn  14215  funcnvs1  14269  pfx2  14304  relexp0g  14376  relexpsucnnr  14379  dfrtrclrec2  14411  rtrclreclem1  14412  rtrclreclem2  14413  rtrclreclem4  14415  dfrtrcl2  14416  climmo  14909  fsumcom2  15124  ackbijnn  15178  incexclem  15186  infcvgaux1i  15207  fprodcom2  15333  bpolylem  15397  bpoly3  15407  bpoly4  15408  efcvgfsum  15434  cos1bnd  15535  cos2bnd  15536  znnen  15560  qnnen  15561  aleph1re  15593  3dvds  15675  n2dvdsm1  15714  n2dvds3OLD  15717  divalglem5  15743  flodddiv4  15759  sadcaddlem  15801  sadadd2lem  15803  sadadd3  15805  sadaddlem  15810  lcmf0  15973  lcmfunsnlem2lem1  15977  lcmfunsnlem2  15979  coprmprod  16000  coprmproddvdslem  16001  2prm  16031  3lcm2e6  16067  phicl2  16100  pockthi  16238  unbenlem  16239  prmrec  16253  vdwlem13  16324  vdwnn  16329  ramcl2  16347  prmgapprmo  16393  mod2xnegi  16402  modsubi  16403  structcnvcnv  16492  setsres  16520  strfv  16526  strleun  16586  0rest  16698  firest  16701  restid  16702  prdsval  16723  prdsbas  16725  prdsplusg  16726  prdsmulr  16727  prdsvsca  16728  imasaddfnlem  16796  imasvscafn  16805  oppchomfval  16979  oppcbas  16983  2oppchomf  16989  rescbas  17094  rescco  17097  rescabs  17098  0ssc  17102  0subcat  17103  idfucl  17146  homarel  17291  dmaf  17304  cdaf  17305  catcfuccl  17364  relxpchom  17426  catcxpccl  17452  oppchofcl  17505  oyoncl  17515  odubas  17738  letsr  17832  mgmidmo  17865  pwmnd  18047  releqg  18272  ga0  18373  oppglem  18423  psgnunilem3  18560  psgnunilem4  18561  pmtrsn  18583  efgval  18779  efger  18780  efgsval2  18795  efgsp1  18799  efgsfo  18801  efgredleme  18805  efgredlem  18809  efgred  18810  cygctb  18948  gsum2d2lem  19029  gsum2d2  19030  gsumcom2  19031  dprd2d2  19102  pgpfaclem1  19139  mgplem  19180  mgpress  19186  opprlem  19314  reldvdsr  19330  00lsp  19689  sralem  19885  srasca  19889  sravsca  19890  psrvscafval  20105  opsrbaslem  20193  psrbag0  20209  00ply1bas  20343  ply1plusgfvi  20345  cnfldfun  20492  cnfldfunALT  20493  xrsmgm  20515  zlmsca  20603  znbaslem  20620  resubdrg  20687  ocv0  20756  cssval  20761  thlbas  20775  thlle  20776  islinds2  20892  matsca  20959  m2detleib  21175  tgdom  21521  tgidm  21523  indistps2ALT  21557  restbas  21701  resttopon  21704  rest0  21712  leordtval2  21755  iocpnfordt  21758  icomnfordt  21759  iooordt  21760  ist1-3  21892  1stcfb  21988  comppfsc  22075  1stckgen  22097  ptbasfi  22124  dfac14  22161  opnfbas  22385  hauspwpwf1  22530  alexsubALT  22594  ptcmplem5  22599  cnextrel  22606  ust0  22762  tuslem  22810  0met  22910  prdsdsf  22911  prdsxmetlem  22912  prdsmet  22914  setsmsbas  23019  setsmsds  23020  prdsbl  23035  tngds  23191  qtopbaslem  23301  xrtgioo  23348  xrsdsre  23352  zcld  23355  recld2  23356  reperflem  23360  retopconn  23371  iccpnfcnv  23482  bndth  23496  nmoleub2lem2  23654  zclmncvs  23686  recmet  23860  resscdrg  23895  ishl2  23907  recms  23917  volf  24064  iundisj2  24084  volsup  24091  icombl  24099  ioombl  24100  ismbf3d  24189  0plef  24207  0pledm  24208  itg1ge0  24221  mbfi1fseqlem5  24254  itg2addlem  24293  reldv  24402  limciun  24426  dvexp  24484  dveflem  24510  lhop1lem  24544  lhop  24547  elply2  24720  elplyd  24726  ply1term  24728  ply0  24732  plymullem  24740  qaa  24846  pserulm  24944  pserdvlem2  24950  efcn  24965  sincosq1lem  25017  tangtx  25025  sincos4thpi  25033  pigt3  25037  pige3ALT  25039  efif1olem4  25061  logf1o  25080  relogf1o  25082  log1  25101  loge  25102  relogiso  25113  dvrelog  25152  relogcn  25153  logcn  25162  cxpcn3  25261  resqrtcn  25262  2logb9irr  25305  leibpi  25453  log2ublem1  25457  birthday  25465  emcllem5  25510  harmonicbnd  25514  harmonicbnd2  25515  harmonicbnd3  25518  lgamgulm2  25546  lgamcvglem  25550  gamf  25553  ppiltx  25687  ppiublem1  25711  ppiub  25713  bclbnd  25789  bpos1lem  25791  bposlem8  25800  lgsquadlem2  25890  2sqlem9  25936  2sqlem10  25937  addsqnreup  25952  chebbnd1  25981  selberg2lem  26059  pntrsumo1  26074  selbergsb  26084  pntpbnd  26097  istrkg2ld  26179  tgcgr4  26250  ttgval  26594  ttglem  26595  cchhllem  26606  ax5seglem7  26654  axlowdimlem4  26664  axlowdimlem6  26666  axlowdimlem7  26667  axlowdimlem10  26670  axlowdimlem13  26673  axlowdimlem16  26676  uhgr0e  26789  uhgr0  26791  upgrbi  26811  umgrbi  26819  usgr0  26958  lfuhgr1v0e  26969  usgrexmpllem  26975  usgrexmpl  26978  griedg0prc  26979  cplgr0  27140  usgrexilem  27155  cffldtocusgr  27162  rgrusgrprc  27304  rusgrprc  27305  rgrprcx  27307  rgrx0ndm  27308  usgr2pthlem  27477  pthdlem2  27482  uspgrn2crct  27519  wwlksnext  27604  wwlksnfi  27617  wwlksnfiOLD  27618  disjxwwlkn  27625  clwwlknondisj  27823  0ewlk  27826  0wlk  27828  0pth  27837  1pthdlem1  27847  1trld  27854  wlk2v2elem2  27868  wlk2v2e  27869  upgr3v3e3cycl  27892  upgr4cycl4dv4e  27897  dfconngr1  27900  0conngr  27904  konigsbergumgr  27963  2wspmdisj  28049  2clwwlk2clwwlk  28062  numclwwlk3lem2lem  28095  numclwwlk3lem2  28096  ex-dif  28135  ex-in  28137  ex-eprel  28145  ex-id  28146  ex-fl  28159  ex-mod  28161  ex-hash  28165  ex-fpar  28174  avril1  28175  2bornot2b  28176  0vfval  28316  vsfval  28343  ajmoi  28568  ajfuni  28569  normlem2  28821  norm3adifii  28858  hhip  28887  hlim0  28945  hlimcaui  28946  hlimf  28947  hhssnv  28974  shscli  29027  shsval2i  29097  h1de2i  29263  fh3i  29333  fh4i  29334  cm2mi  29336  qlaxr3i  29346  mayetes3i  29439  ho0f  29461  hoif  29464  hodidi  29497  ho0subi  29505  hosd1i  29532  adjmo  29542  nmopsetn0  29575  nmfnsetn0  29588  funadj  29596  funcnvadj  29603  nmcexi  29736  cnlnadjlem8  29784  nmoptri2i  29809  opsqrlem4  29853  hmopidmchi  29861  pjoci  29890  pjinvari  29901  abrexdomjm  30200  elim2ifim  30233  iundisj2f  30274  rinvf1o  30309  dfcnv2  30356  snct  30381  fzodif2  30447  iundisj2fi  30452  dp2lt10  30493  dp2ltc  30496  dplti  30514  dpgti  30515  dpexpp1  30517  gsumle  30658  xrge0slmod  30850  xrge0pluscn  31088  zlmds  31110  zlmtset  31111  qqhre  31166  esumrnmpt2  31232  esumfsup  31234  esumpcvgval  31242  hasheuni  31249  esumcvg  31250  esumcvgsum  31252  esumsup  31253  esum2d  31257  dmsigagen  31308  ldgenpisyslem3  31329  measvuni  31378  voliune  31393  volfiniune  31394  br2base  31432  dya2iocuni  31446  eulerpartlem1  31530  eulerpartlemt  31534  eulerpartgbij  31535  fib0  31562  coinfliprv  31645  ballotlem2  31651  ballotlemic  31669  ballotlem7  31698  ballotth  31700  plymul02  31721  rpsqrtcn  31769  chtvalz  31805  circlemethnat  31817  circlevma  31818  circlemethhgt  31819  hgt750lem  31827  bnj226  31909  bnj1101  31961  bnj110  32035  bnj149  32052  bnj150  32053  bnj151  32054  bnj517  32062  bnj580  32090  bnj865  32100  bnj900  32106  bnj996  32132  bnj1110  32157  bnj1133  32164  bnj1128  32165  bnj1145  32168  bnj1137  32170  bnj1171  32175  bnj1176  32180  f1resfz0f1d  32264  subfacp1lem5  32334  subfacp1lem6  32335  kur14lem9  32364  cvmcov2  32425  cvmliftlem1  32435  cvmliftlem4  32438  cvmliftlem5  32439  gonanegoal  32502  satfv0  32508  satfv0fun  32521  fmlan0  32541  gonan0  32542  fmla0disjsuc  32548  ex-sategoelel12  32577  msrfo  32696  problem5  32815  brtpid1  32854  brtpid2  32855  brtpid3  32856  logi  32869  faclimlem1  32878  axextndbi  32952  poseq  32998  sltval2  33066  noxp1o  33073  nosepnelem  33087  txprel  33243  relsset  33252  relbigcup  33261  fvbigcup  33266  fnsingle  33283  fvsingle  33284  snelsingles  33286  funimage  33292  fullfunfnv  33310  imagesset  33317  funtransport  33395  colinrel  33421  funray  33504  funline  33506  0hf  33541  neibastop2lem  33611  filnetlem3  33631  nrmo  33661  waj-ax  33665  lukshef-ax2  33666  arg-ax  33667  limsucncmpi  33696  dnizeq0  33717  knoppcnlem8  33742  knoppcnlem11  33745  cnndvlem1  33779  bj-babylob  33841  bj-ax12ssb  33894  bj-nnfnth  33975  bj-disjcsn  34166  bj-snsetex  34178  bj-0eltag  34193  bj-2upln0  34238  bj-2upln1upl  34239  bj-isrvec  34469  f1omptsnlem  34505  f1omptsn  34506  icoreresf  34521  relowlssretop  34532  relowlpssretop  34533  domalom  34573  matunitlindf  34776  poimirlem3  34781  poimirlem9  34787  poimirlem16  34794  poimirlem17  34795  poimirlem18  34796  poimirlem19  34797  poimirlem20  34798  poimirlem26  34804  mblfinlem1  34815  mblfinlem2  34816  ismblfin  34819  voliunnfl  34822  cnambfre  34826  abrexdom  34892  fdc  34907  cncfres  34930  heibor1lem  34974  grposnOLD  35047  bicontr  35245  an12i  35263  tsim1  35295  ac6s6f  35338  vvdifopab  35408  brcnvrabga  35486  opabf  35506  xrnrel  35511  relcoels  35555  cnvcosseq  35568  refrelcoss3  35589  refrelcoss2  35590  symrelcoss2  35592  refrelcoss  35648  symrelcoss  35682  n0eldmqs  35769  ax13fromc9  35928  dedths  35984  renegclALT  35985  hlhilslem  38960  sn-axprlem3  38993  rtprmirr  39078  dffltz  39155  moxfr  39173  mapfzcons1  39198  diophrw  39240  0dioph  39259  vdioph  39260  rabren3dioph  39296  2nn0ind  39426  rpnnen3  39513  kelac2lem  39548  frlmpwfi  39582  ifpbiidcor2  39733  iscard4  39784  eliunov2  39908  xphe  40011  0he  40012  he0  40014  snhesn  40016  idhe  40017  frege54cor1c  40145  clsk1independent  40280  neicvgnvor  40350  amgm2d  40436  amgm3d  40437  amgm4d  40438  lhe4.4ex1a  40545  rusbcALT  40655  ipo0  40665  ifr0  40666  vk15.4j  40746  2sb5nd  40778  dfvd1ir  40791  dfvd2anir  40802  dfvd2ir  40804  dfvd3ir  40811  dfvd3anir  40814  iden2  40832  e0bir  40995  uun2221p1  41032  uun2221p2  41033  2sb5ndVD  41128  2sb5ndALT  41150  iunconnlem2  41153  fnchoice  41170  unisn0  41200  eliincex  41261  icof  41366  supminfxr  41624  fsumiunss  41740  climlimsupcex  41934  liminfltlimsupex  41946  liminflelimsupcex  41962  xlimrel  41985  xlimfun  42020  resincncf  42042  dvnprodlem3  42117  volioc  42141  volico  42153  dmvolss  42155  volioof  42157  stoweidlem13  42183  stoweidlem34  42204  stirlinglem5  42248  stirlinglem13  42256  stirlingr  42260  fourierdlem42  42319  fourierdlem62  42338  fouriersw  42401  etransc  42453  salexct  42502  salexct2  42507  salgencntex  42511  sge0rnn0  42535  gsumge0cl  42538  sge00  42543  sge0resplit  42573  sge0reuz  42614  omeiunle  42684  0ome  42696  icoresmbl  42710  ovn0lem  42732  ovnhoilem1  42768  hspmbl  42796  ovolval5lem3  42821  nsssmfmbf  42940  mbfpsssmf  42944  smfresal  42948  smfmullem4  42954  smfpimbor1lem1  42958  smfpimbor1lem2  42959  aistia  43018  aisfina  43019  aiffnbandciffatnotciffb  43025  axorbciffatcxorb  43026  abnotbtaxb  43036  abnotataxb  43037  eusnsn  43146  aiotaval  43178  aiota0ndef  43180  ichv  43460  ichf  43461  ichid  43462  ichcircshi  43463  icheq  43471  spr0nelg  43489  m3prm  43605  m7prm  43615  0noddALTV  43705  2noddALTV  43709  341fppr2  43750  9fppr8  43753  nfermltl8rev  43758  nfermltl2rev  43759  nfermltlrev  43760  sbgoldbo  43803  nnsum3primes4  43804  evengpop3  43814  oddinmgm  43933  nn0mnd  43937  efmndmgm  43956  smndex1ibas  43974  smndex1mgm  43981  smndex1mnd  43984  smndex2dbas  43988  smndex2dnrinv  43989  smndex2hbas  43990  2zrngamgm  44112  2zrngaabl  44117  2zrngmmgm  44119  2zrngnring  44125  fldhmsubc  44257  fldhmsubcALTV  44275  eliunxp2  44284  zlmodzxzldeplem  44455  zlmodzxzldep  44461  ldepslinc  44466  rrx2xpreen  44608  rrx2plordisom  44612  line2ylem  44640  line2  44641  line2x  44643  inlinecirc02plem  44675  ex-gte  44730  empty-surprise  44785  eximp-surprise2  44788  amgmw2d  44807
  Copyright terms: Public domain W3C validator