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

Theorem impbid2 216
Description: Infer an equivalence from two implications. (Contributed by NM, 6-Mar-2007.) (Proof shortened by Wolf Lammen, 27-Sep-2013.)
Hypotheses
Ref Expression
impbid2.1 (𝜓𝜒)
impbid2.2 (𝜑 → (𝜒𝜓))
Assertion
Ref Expression
impbid2 (𝜑 → (𝜓𝜒))

Proof of Theorem impbid2
StepHypRef Expression
1 impbid2.2 . . 3 (𝜑 → (𝜒𝜓))
2 impbid2.1 . . 3 (𝜓𝜒)
31, 2impbid1 215 . 2 (𝜑 → (𝜒𝜓))
43bicomd 213 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:  biimt  350  biorf  420  biorfiOLD  423  pm4.72  919  biort  937  bimsc1  979  19.38a  1765  19.38b  1766  ax13b  1962  cgsexg  3233  cgsex2g  3234  cgsex4g  3235  elab3gf  3350  abidnf  3369  elsn2g  4201  eqoreldif  4216  difsn  4319  eqsnOLD  4353  prel12  4374  elpreqprb  4388  dfnfc2  4445  dfnfc2OLD  4446  intmin4  4497  dfiin2g  4544  elpw2g  4818  ssrel  5197  ssrelOLD  5198  ssrel2  5200  ssrelrel  5210  releldmb  5349  relelrnb  5350  cnveqb  5578  dmsnopg  5594  relcnvtr  5643  elsnxp  5665  ord0eln0  5767  f1ocnvb  6137  ffvresb  6380  isof1oopb  6560  soisores  6562  riotaclb  6634  fnoprabg  6746  difex2  6954  dfwe2  6966  ordpwsuc  7000  ordunisuc2  7029  limsssuc  7035  dfom2  7052  relcnvexb  7099  dfsmo2  7429  omord  7633  nneob  7717  pw2f1olem  8049  sucdom  8142  fundmfibi  8230  f1dmvrnfibi  8235  fieq0  8312  hartogslem1  8432  rankr1ag  8650  rankeq0b  8708  fidomtri  8804  fidomtri2  8805  isfin2-2  9126  enfin2i  9128  isfin3-2  9174  isf34lem6  9187  isfin1-2  9192  isfin1-3  9193  isfin7-2  9203  axgroth6  9635  ltsonq  9776  ltexnq  9782  znegclb  11399  rpneg  11848  nltpnft  11980  ngtmnft  11982  xrrebnd  11984  qextlt  12019  qextle  12020  iccneg  12278  fzsn  12368  fz1sbc  12400  fzofzp1b  12550  ceilidz  12634  fleqceilz  12636  hashclb  13132  hashnncl  13140  hashfun  13207  reim0b  13840  rexanre  14067  rexuzre  14073  lo1resb  14276  o1resb  14278  dvdsext  15024  zob  15064  ncoprmgcdne1b  15344  pceq0  15556  pc11  15565  pcz  15566  ramtcl  15695  cshwsiun  15787  pospo  16954  oduposb  17117  cnvpsb  17194  tsrlemax  17201  issubg2  17590  issubg4  17594  ghmmhmb  17652  pmtrmvd  17857  mndodcong  17942  issubrg2  18781  lpigen  19237  cyggic  19902  ip2eq  19979  maducoeval2  20427  eltg3  20747  bastop  20766  0top  20768  iscld3  20849  isclo2  20873  cnprest  21074  dfconn2  21203  comppfsc  21316  cmphaushmeo  21584  reghaus  21609  nrmhaus  21610  fbun  21625  fsubbas  21652  ufileu  21704  uffix  21706  txflf  21791  fclsrest  21809  flimfnfcls  21813  ptcmplem2  21838  tgpt1  21902  tgpt0  21903  isngp2  22382  nrgdomn  22456  nmhmcn  22901  iscmet3  23072  limcflf  23626  ply1nzb  23863  coe11  23990  dgreq0  24002  eldmgm  24729  sqf11  24846  sqff1o  24889  zabsle1  25002  lgsabs1  25042  lgsquadlem2  25087  issubgr2  26145  uhgrissubgr  26148  usgrfilem  26200  uvtxnbgrb  26283  cusgrfilem3  26334  vdiscusgr  26408  wwlksn0s  26727  nmobndi  27600  hmopadj2  28770  mdslle1i  29146  mdslle2i  29147  relfi  29387  ssrelf  29397  prodindf  30059  bnj1173  31044  resconn  31202  cvmsval  31222  elmrsubrn  31391  funsseq  31642  brcolinear  32141  outsideofeu  32213  lineunray  32229  nn0prpw  32293  bj-19.3t  32664  bj-sb3b  32779  bj-sngltag  32946  bj-elid2  33057  bj-inftyexpiinj  33067  wl-sb5nae  33311  wl-ax11-lem2  33334  poimirlem26  33406  poimirlem27  33407  heicant  33415  cover2  33479  eqfnun  33487  isbndx  33552  isbnd2  33553  equivbnd2  33562  prdsbnd2  33565  elghomlem2OLD  33656  isdrngo3  33729  riotaclbgBAD  34059  lssatle  34121  opcon3b  34302  cdlemk33N  36016  cdlemk34  36017  wepwsolem  37431  rp-fakeimass  37676  cnvssb  37711  intimag  37767  sscon34b  38137  ntrneiiso  38209  pm11.71  38417  pm14.122b  38444  pm14.123b  38447  iotavalb  38451  eliuniin  39099  eliuniin2  39123  climreeq  39645  rexrsb  40932  reuan  40943  afv0nbfvbi  40994  dfafn5b  41004  elfz2z  41088  zeo2ALTV  41347  nnlog2ge0lt1  42125
  Copyright terms: Public domain W3C validator