Theorem mpbiri 258

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

Step	Hyp	Ref	Expression
1		mpbiri.min	. . 3 ⊢ 𝜒
2	1	a1i 11	. 2 ⊢ (𝜑 → 𝜒)
3		mpbiri.maj	. 2 ⊢ (𝜑 → (𝜓 ↔ 𝜒))
4	2, 3	mpbird 257	1 ⊢ (𝜑 → 𝜓)

Syntax hints:   → wi 4   ↔ wb 205

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 206

This theorem is referenced by:  elimh  1081  spei  2388  nfald2  2439  nfabd2  2924  raleleqALT  3336  dedhb  3696  sbceqalOLD  3840  csbie2df  4436  ssdifeq0  4482  r19.2zb  4491  dedth  4582  pwidg  4618  elpr2OLD  4650  snidg  4658  rexreusng  4679  exsnrex  4680  ifpr  4691  rmosn  4719  rabrsn  4724  prid1g  4760  tpid1g  4769  tpid2g  4771  tpid3g  4772  pwpw0  4812  sssn  4825  elpreqpr  4863  unimax  4942  intmin3  4974  eqbrtrdi  5181  al0ssb  5302  intabs  5338  pwnss  5345  difelpw  5347  rabelpw  5348  0inp0  5353  intidg  5453  copsexgw  5486  copsexg  5487  euotd  5509  elopab  5523  elvvuni  5748  posn  5757  frsn  5759  eqrelriv  5785  relsnb  5798  relopabiALT  5819  opabid2  5824  ididg  5850  iss  6033  dfpo2  6294  ord0eln0  6418  sucidg  6444  nsuceq0  6446  funopg  6581  fn0  6680  f00  6773  f0bi  6774  f10d  6867  f1o00  6868  fo00  6869  brprcneu  6881  brprcneuALT  6882  dffn5  6951  fsn  7138  funop  7152  funsndifnop  7154  fnsnb  7169  eufnfv  7235  f1eqcocnv  7304  f1eqcocnvOLD  7305  nfriotadw  7378  nfriotad  7382  riotaprop  7398  oprabidw  7445  oprabid  7446  elrnmpo  7551  ov6g  7579  ovelrn  7591  caovmo  7652  offn  7692  caofinvl  7709  fr3nr  7768  onprc  7774  ordeleqon  7778  onint0  7788  0elsuc  7832  onuninsuci  7838  orduninsuc  7841  ordzsl  7843  onzsl  7844  tfinds  7858  limomss  7869  limom  7880  peano5  7893  peano5OLD  7894  xpexr  7920  eqop2  8030  opreuopreu  8032  1stconst  8099  2ndconst  8100  frxp2  8143  frxp3  8150  funsssuppss  8188  dftpos3  8243  dftpos4  8244  wfrlem4OLD  8326  wfrlem14OLD  8336  oawordeulem  8568  omwordi  8585  nnmwordi  8649  riiner  8800  ecopover  8831  map0g  8894  mapsnd  8896  elixpsn  8947  en0  9029  en0OLD  9030  en0ALT  9031  en0r  9032  en1  9037  en1OLD  9038  fiprc  9061  sbthlem2  9100  sbthlem4  9102  sbthlem5  9103  0domg  9116  findcard  9179  findcard2  9180  nneneq  9225  nneneqOLD  9237  sdom1  9258  sdom1OLD  9259  1sdom2dom  9263  fineqvlem  9278  nfielex  9289  enp1i  9295  findcard2OLD  9300  elfiun  9445  marypha1lem  9448  oicl  9544  oif  9545  oion  9551  hartogslem1  9557  hartogs  9559  wemapso2  9568  card2on  9569  0wdom  9585  brwdom2  9588  inf3lem6  9648  cantnflem3  9706  cantnflem4  9707  wemapwe  9712  cnfcom  9715  ssttrcl  9730  ttrclselem2  9741  tctr  9755  r1tr  9791  r1rankidb  9819  r1pw  9860  scottex  9900  scott0  9901  bnd2  9908  eldju2ndl  9939  tskwe  9965  oncard  9975  cardlim  9987  harsdom  10010  en2eleq  10023  dfac8alem  10044  cardaleph  10104  iunfictbso  10129  infmap2  10233  ackbij1lem18  10252  cff  10263  cfsuc  10272  cff1  10273  cflim2  10278  cfss  10280  sdom2en01  10317  infpssrlem4  10321  fin23lem7  10331  fin23lem11  10332  isfin2-2  10334  fin23lem26  10340  fin23lem19  10351  fin23lem17  10353  isf34lem2  10388  isf34lem4  10392  fin1a2lem6  10420  fin1a2lem10  10424  fin1a2lem12  10426  itunifn  10432  hsmexlem1  10441  axcc2lem  10451  dcomex  10462  axdc3lem4  10468  ondomon  10578  konigthlem  10583  pwcfsdom  10598  cfpwsdom  10599  axpowndlem3  10614  canth4  10662  canthnumlem  10663  canthwelem  10665  canthwe  10666  canthp1lem2  10668  pwfseqlem4  10677  pwfseqlem5  10678  gchaleph  10686  gch2  10690  winainflem  10708  0tsk  10770  rankcf  10792  tskcard  10796  gruina  10833  grutsk  10837  tskmid  10855  indpi  10922  nqereu  10944  mulcanenq  10975  recmulnq  10979  archnq  10995  ltsopr  11047  1ne0sr  11111  0idsr  11112  00sr  11114  leid  11332  lelttric  11343  divcan3  11920  lemul1a  12090  nn1suc  12256  nn0n0n1ge2b  12562  xnn0xr  12571  xnn0nemnf  12577  nn0lt10b  12646  nn0ind-raph  12684  elnn1uz2  12931  indstr2  12933  uzsupss  12946  rpnnen1lem4  12986  rpnnen1lem5  12987  xrnemnf  13121  xrnepnf  13122  mnfltxr  13131  xnn0n0n1ge2b  13135  xnn0ge0  13137  xrlttri  13142  xrlttr  13143  xrleid  13154  qbtwnxr  13203  xmullem2  13268  xlemul1a  13291  xrub  13315  reltxrnmnf  13345  ixxun  13364  xnn0xrge0  13507  fztpval  13587  fseq1p1m1  13599  elfznelfzob  13762  ltweuz  13950  fzfi  13961  fsuppmapnn0fiubex  13981  ser0f  14044  0exp  14086  faclbnd4lem1  14276  bcn1  14296  hashnemnf  14327  hashv01gt1  14328  hashsnle1  14400  hashgt12el2  14406  hashpw  14419  hashf1  14442  fz1isolem  14446  hash2prb  14457  0wrd0  14514  wrdlen1  14528  ccatvalfn  14555  eqs1  14586  wrdl1exs1  14587  swrdlen  14621  swrdwrdsymb  14636  swrdspsleq  14639  cats1un  14695  wrdind  14696  wrd2ind  14697  swrdccatin1  14699  repswsymballbi  14754  cshw1  14796  scshwfzeqfzo  14801  wrdl2exs2  14921  trclfvcotr  14980  relexp1g  14997  relexp0rel  15008  relexprelg  15009  relexpreld  15011  sqrt0  15212  sqrtsq  15240  mptfzshft  15748  prodf1f  15862  egt2lt3  16174  0dvds  16245  nn0onn  16348  nn0o  16351  divalgmod  16374  flodddiv4  16381  bitsp1o  16399  gcddvds  16469  bezout  16510  lcmdvds  16570  rpdvds  16622  1nprm  16641  prmind2  16647  dvdszzq  16684  nnoddn2prmb  16773  pcpre1  16802  vdwapf  16932  vdwapid1  16935  ram0  16982  ramz  16985  prmolefac  17006  cshws0  17062  prmlem0  17066  strle1  17118  restsspw  17404  prdsdsfn  17438  imasdsfn  17487  imasaddfnlem  17501  imasvscafn  17510  xpsfrnel  17535  isacs1i  17628  cidfn  17650  fnhomeqhomf  17662  comffn  17676  isoval  17739  sscres  17797  cofucl  17865  idffth  17913  ressffth  17918  cat1lem  18076  catcoppccl  18097  catcoppcclOLD  18098  estrchomfn  18116  funcestrcsetclem4  18125  funcestrcsetclem7  18128  equivestrcsetc  18134  funcsetcestrclem4  18140  funcsetcestrclem7  18143  1stfcl  18179  2ndfcl  18180  prfcl  18185  evlfcl  18205  curf1cl  18211  curfcl  18215  hofcl  18242  yonedainv  18264  pospo  18328  lubfun  18335  glbfun  18348  joindmss  18362  meetdmss  18376  ipopos  18519  acsficl2d  18535  dirref  18584  mgmidcl  18617  mgmlrid  18618  ielefmnd  18830  smndex1basss  18848  smndex1n0mnd  18855  cntzssv  19270  idresperm  19331  symgvalstruct  19342  symgvalstructOLD  19343  pmtrfmvdn0  19408  symggen  19416  psgnunilem1  19439  psgnprfval  19467  slwpgp  19559  frgpmhm  19711  frgpuptinv  19717  frgpup3lem  19723  gsumzoppg  19890  gsumcom2  19921  c0snmhm  20391  srhmsubc  20602  rhmsubclem1  20607  abv0  20700  rrgsupp  21227  zrhrhm  21424  psgnodpmr  21509  frlmphllem  21701  ellspd  21723  psrvscafval  21878  psrridm  21893  ltbwe  21969  psrbag0  21993  psrbagsn  21994  subrgascl  21997  psdmul  22077  mattpostpos  22343  mavmul0  22441  mavmul0g  22442  mdet0f1o  22482  m1detdiag  22486  m2detleiblem5  22514  m2detleiblem6  22515  m2detleiblem3  22518  m2detleiblem4  22519  maducoeval2  22529  d1mat2pmat  22628  chpmat1dlem  22724  chpmat1d  22725  baspartn  22844  eltg3  22852  topnex  22886  fctop  22894  cctop  22896  discld  22980  mretopd  22983  neipeltop  23020  neitr  23071  restcls  23072  ordtbaslem  23079  ordtuni  23081  idcn  23148  cnrmi  23251  cmpsublem  23290  cmpsub  23291  tgcmp  23292  uncmp  23294  hauscmplem  23297  cmpfi  23299  bwth  23301  1stcrestlem  23343  disllycmp  23389  dis1stc  23390  refref  23404  kgeni  23428  1stckgenlem  23444  kqffn  23616  snfil  23755  filconn  23774  cfinfil  23784  ufileu  23810  filufint  23811  fixufil  23813  cfinufil  23819  ufilen  23821  fin1aufil  23823  fmf  23836  rnelfm  23844  flimclslem  23875  hauspwpwf1  23878  supnfcls  23911  flimfnfcls  23919  fclscmp  23921  alexsubALTlem2  23939  alexsubALTlem3  23940  alexsubALT  23942  ptcmplem1  23943  cnextrel  23954  tsmsfbas  24019  ustref  24110  trust  24121  restutop  24129  isusp  24153  xmet0  24235  imasdsf1olem  24266  blfvalps  24276  blfps  24299  blf  24300  restmetu  24466  dscmet  24468  isngp2  24493  nm0  24525  nrginvrcn  24596  nmoix  24633  qdensere  24673  iccconn  24733  iccpnfcnv  24856  xrhmeo  24858  lebnumlem3  24876  metsscmetcld  25230  bcthlem5  25243  csschl  25291  rrxmfval  25321  minveclem3b  25343  cniccbdd  25377  ovolicc2lem4  25436  iunmbl  25469  ioorinv  25492  ioorcl  25493  i1f1lem  25605  limcvallem  25787  ellimc2  25793  limccnp  25807  limccnp2  25808  limcco  25809  perfdvf  25819  recnprss  25820  fncpn  25850  dvcmulf  25863  c1lip1  25917  lhop2  25935  q1pcl  26079  r1pdeglt  26082  ply1remlem  26086  plyssc  26121  ulm0  26314  cxpeq0  26599  cxplea  26617  cxplogb  26705  asinlem  26787  isppw2  27034  muval2  27053  dchrfi  27175  dchrpt  27187  bposlem6  27209  lgsdir2lem2  27246  lgsqr  27271  gausslemma2dlem4  27289  2lgslem2  27315  2lgslem3  27324  2lgs  27327  2sqlem7  27344  2sqlem11  27349  chtppilim  27395  nosgnn0i  27579  nolesgn2ores  27592  nogesgn1ores  27594  nosepnelem  27599  nosepdmlem  27603  nosupbnd1lem3  27630  nosupbnd1lem5  27632  nosupbnd2lem1  27635  noinfbnd1lem3  27645  noinfbnd1lem5  27647  noinfbnd2lem1  27650  oldval  27768  made0  27787  lrrecpo  27845  pncan2s  27969  abssor  28127  om2noseqfo  28158  noseqrdglem  28165  noseqrdgfn  28166  noseqrdg0  28167  n0scut  28190  tgldimor  28293  tgcgr4  28322  tglnfn  28338  tglnunirn  28339  mirne  28458  mircinv  28459  perpln1  28501  perpln2  28502  lmiisolem  28587  xmstrkgc  28683  axcgrtr  28713  axsegconlem9  28723  axlowdimlem5  28744  axlowdimlem17  28756  axlowdim1  28757  uhgr0e  28871  edglnl  28943  uhgr0edgfi  29040  issubgr2  29072  subgrprop2  29074  egrsubgr  29077  0grsubgr  29078  0uhgrsubgr  29079  uhgrsubgrself  29080  nbgr0vtx  29156  nbgr1vtx  29158  nbgrssovtx  29161  nb3grprlem1  29180  uvtx01vtx  29197  cplgr1vlem  29229  cplgr1v  29230  usgrexilem  29240  wlkcomp  29432  wlk1walk  29440  wlkp1lem5  29478  uhgrwkspthlem1  29554  pthdlem1  29567  clwlkcomp  29580  lfgrn1cycl  29603  uspgrn2crct  29606  wwlksn0s  29659  umgrwwlks2on  29755  clwwlkn  29823  clwwlkn1  29838  0ewlk  29911  1ewlk  29912  0spth  29923  upgr1wlkdlem2  29943  wlk2v2e  29954  upgr3v3e3cycl  29977  upgr4cycl4dv4e  29982  eupth0  30011  frgr0v  30059  frgr1v  30068  1vwmgr  30073  ex-opab  30229  grpoinvf  30329  nvmid  30456  nmlnoubi  30593  hiidrcl  30892  hsn0elch  31045  shjshseli  31290  cmbr4i  31398  dfiop2  31550  kbpj  31753  nmopun  31811  adjeq0  31888  kbass2  31914  pjssdif1i  31972  pjinvari  31988  pjcmul2i  31999  pj3i  32005  stge1i  32035  stle0i  32036  sumdmdlem2  32216  dmdbr6ati  32220  dmdbr7ati  32221  rabsnel  32284  unidifsnel  32316  unidifsnne  32317  disjdifprg  32350  ofoprabco  32433  padct  32485  fpwrelmapffslem  32498  xrlelttric  32506  xnn0gt0  32523  iundisj2cnt  32551  f1ocnt  32554  fz1nnct  32555  fz1nntr  32556  hashxpe  32560  nn0min  32565  wrdt2ind  32656  xrge0tsmsbi  32750  opprabs  33129  locfinref  33378  dispcmp  33396  zartopn  33412  zarcmplem  33418  pstmxmet  33434  xrge0iifcnv  33470  xrge0iif1  33475  qqhre  33557  esumcl  33585  esumpr2  33622  esumpinfval  33628  esumpcvgval  33633  ofcfn  33655  pwsiga  33685  prsiga  33686  sigainb  33691  ldgenpisyslem1  33718  measiuns  33772  relfae  33802  pmeasmono  33880  sitgf  33903  eulerpartgbij  33928  sgnmulsgn  34105  sgnmulsgp  34106  signswch  34129  signslema  34130  signstlen  34135  signstfvn  34137  circlevma  34210  bnj216  34299  bnj151  34444  bnj517  34452  bnj970  34514  bnj1145  34560  bnj1498  34628  fineqvrep  34651  fineqvac  34653  0nn0m1nnn0  34658  pthhashvtx  34673  acycgr0v  34694  prclisacycgr  34697  umgracycusgr  34700  cusgracyclt3v  34702  subfacp1lem5  34730  erdszelem8  34744  kur14lem1  34752  indispconn  34780  cvmsss2  34820  satfvsuclem2  34906  satfrel  34913  satfrnmapom  34916  satfv0fun  34917  satf00  34920  satf0suclem  34921  fmlasuc0  34930  msubrn  35075  dfon2lem7  35321  brbigcup  35430  elsingles  35450  fnimage  35461  funpartlem  35474  dfrdg4  35483  imagesset  35485  altopthsn  35493  elaltxp  35507  ellines  35684  linethru  35685  rankeq1o  35703  elhf2  35707  hfninf  35718  nn0prpwlem  35742  fneref  35770  neibastop2lem  35780  limsucncmpi  35865  bj-exlimmpbir  36328  curryset  36361  bj-snglex  36388  bj-restpw  36507  bj-inftyexpidisj  36625  topdifinffinlem  36762  relowlssretop  36778  rdgeqoa  36785  finxpreclem6  36811  fvineqsneq  36827  pibt2  36832  poimirlem23  37051  poimirlem29  37057  poimirlem31  37059  volsupnfl  37073  cnambfre  37076  dvasin  37112  dvacos  37113  sdclem2  37150  sstotbnd2  37182  ssbnd  37196  ismgmOLD  37258  grpokerinj  37301  rngomndo  37343  isdrngo1  37364  ac6s6  37580  iss2  37752  cnvelrels  37904  cosselrels  37905  brssrid  37911  brcnvssrid  37916  dfdisjs5  38121  eldisjs5  38135  mpets2  38250  pets  38261  prtlem12  38276  riotasv2d  38366  lkrscss  38507  islshpkrN  38529  isline  39149  ispointN  39152  0psubN  39159  linepsubN  39162  atpsubN  39163  cdlemk36  40323  diafn  40444  dibfna  40564  dibvalrel  40573  dicvalrelN  40595  diclspsn  40604  dihvalrel  40689  dih1  40696  lclkrlem1  40916  lclkr  40943  mapd1o  41058  mapdin  41072  hdmapfnN  41239  hgmapfnN  41298  lcmineqlem10  41446  sticksstones9  41558  sn-iotalem  41629  repncan2  41859  sn-inelr  41942  elrfirn  42037  ismrcd1  42040  istopclsd  42042  rabren3dioph  42157  jm2.17b  42304  jm2.22  42338  jm2.23  42339  ttac  42379  pw2f1ocnv  42380  dnnumch1  42390  hbtlem5  42474  mncn0  42485  aaitgo  42508  rngunsnply  42519  unielss  42569  onexlimgt  42594  cantnfresb  42676  dflim5  42681  naddwordnexlem4  42754  safesnsupfiss  42768  safesnsupfidom1o  42770  safesnsupfilb  42771  ensucne0OLD  42883  clcnvlem  42976  relexp01min  43066  ntrf  43476  ssrecnpr  43668  seff  43669  sblpnf  43670  nzss  43677  dvconstbi  43694  ipo0  43809  ifr0  43810  addrfn  43832  subrfn  43833  mulvfn  43834  refsum2cnlem1  44322  rn1st  44573  ellimciota  44925  dvmptconst  45226  dvmptidg  45228  dvmulcncf  45236  dvdivcncf  45238  stoweidlem26  45337  stoweidlem50  45361  stoweidlem57  45368  aiotaval  46398  ndfatafv2nrn  46524  afv2ndefb  46527  funop1  46586  fun2dmnopgexmpl  46587  2ffzoeq  46631  iccpartiltu  46685  iccpartigtl  46686  zofldiv2ALTV  46925  evenprm2  46977  9fppr8  47000  stgoldbwt  47039  nnsum3primesle9  47057  nnsum4primeseven  47063  nnsum4primesevenALTV  47064  tgblthelfgott  47078  uspgrex  47135  0mgm  47151  nnsgrpmgm  47161  rngchomffvalALTV  47263  rhmsubcALTVlem1  47266  funcringcsetcALTV2lem4  47278  funcringcsetclem4ALTV  47301  srhmsubcALTV  47310  mapsnop  47331  zlmodzxzldeplem4  47494  zofldiv2  47527  fdivval  47535  nnlog2ge0lt1  47562  dig1  47604  itcoval2  47660  itcoval3  47661  mosn  47806  mo0  47807  mof02  47814  mofeu  47823  f102g  47827  f1mo  47828  f1omo  47836  intubeu  47918  unilbeu  47919  functhinclem1  47970  fullthinc  47975  thincciso  47978  indthinc  47981  indthincALT  47982