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  349  biorf  419  biorfiOLD  422  pm4.72  956  biort  974  bimsc1  1017  19.38a  1904  19.38b  1905  ax13b  2103  cgsexg  3366  cgsex2g  3367  cgsex4g  3368  elab3gf  3484  abidnf  3504  elsn2g  4343  eqoreldif  4357  difsn  4461  eqsnOLD  4495  prel12OLD  4515  elpreqprb  4536  dfnfc2  4594  dfnfc2OLD  4595  intmin4  4646  dfiin2g  4693  elpw2g  4964  ssrel  5352  ssrelOLD  5353  ssrel2  5355  ssrelrel  5365  releldmb  5503  relelrnb  5504  cnveqb  5736  dmsnopg  5753  relcnvtr  5804  elsnxp  5826  ord0eln0  5928  f1ocnvb  6299  ffvresb  6545  isof1oopb  6726  soisores  6728  riotaclb  6800  fnoprabg  6914  difex2  7122  dfwe2  7134  ordpwsuc  7168  ordunisuc2  7197  limsssuc  7203  dfom2  7220  relcnvexb  7267  dfsmo2  7601  omord  7805  nneob  7889  pw2f1olem  8217  sucdom  8310  fundmfibi  8398  f1dmvrnfibi  8403  fieq0  8480  hartogslem1  8600  rankr1ag  8826  rankeq0b  8884  fidomtri  8980  fidomtri2  8981  isfin2-2  9304  enfin2i  9306  isfin3-2  9352  isf34lem6  9365  isfin1-2  9370  isfin1-3  9371  isfin7-2  9381  axgroth6  9813  ltsonq  9954  ltexnq  9960  znegclb  11577  rpneg  12027  nltpnft  12159  ngtmnft  12161  xrrebnd  12163  qextlt  12198  qextle  12199  iccneg  12457  fzsn  12547  fz1sbc  12580  fzofzp1b  12731  ceilidz  12816  fleqceilz  12818  hashclb  13312  hashnncl  13320  hashfun  13387  reim0b  14029  rexanre  14256  rexuzre  14262  lo1resb  14465  o1resb  14467  dvdsext  15216  zob  15256  ncoprmgcdne1b  15536  pceq0  15748  pc11  15757  pcz  15758  ramtcl  15887  cshwsiun  15979  pospo  17145  oduposb  17308  cnvpsb  17385  tsrlemax  17392  issubg2  17781  issubg4  17785  ghmmhmb  17843  pmtrmvd  18047  mndodcong  18132  issubrg2  18973  lpigen  19429  cyggic  20094  ip2eq  20171  maducoeval2  20619  eltg3  20939  bastop  20958  0top  20960  iscld3  21041  isclo2  21065  cnprest  21266  dfconn2  21395  comppfsc  21508  cmphaushmeo  21776  reghaus  21801  nrmhaus  21802  fbun  21816  fsubbas  21843  ufileu  21895  uffix  21897  txflf  21982  fclsrest  22000  flimfnfcls  22004  ptcmplem2  22029  tgpt1  22093  tgpt0  22094  isngp2  22573  nrgdomn  22647  nmhmcn  23091  iscmet3  23262  limcflf  23815  ply1nzb  24052  coe11  24179  dgreq0  24191  eldmgm  24918  sqf11  25035  sqff1o  25078  zabsle1  25191  lgsabs1  25231  lgsquadlem2  25276  issubgr2  26334  uhgrissubgr  26337  usgrfilem  26389  uvtxnbgrb  26477  nbusgrvtxm1uvtx  26481  cusgrfilem3  26534  vdiscusgr  26608  wwlksn0s  26941  clwwlknon1loop  27217  clwwlknun  27232  nmobndi  27910  hmopadj2  29080  mdslle1i  29456  mdslle2i  29457  relfi  29693  ssrelf  29705  prodindf  30365  bnj1173  31348  resconn  31506  cvmsval  31526  elmrsubrn  31695  funsseq  31944  brcolinear  32443  outsideofeu  32515  lineunray  32531  nn0prpw  32595  bj-19.3t  32966  bj-sb3b  33081  bj-sngltag  33248  bj-elid2  33368  bj-inftyexpiinj  33378  wl-sb5nae  33622  wl-ax11-lem2  33645  poimirlem26  33717  poimirlem27  33718  heicant  33726  cover2  33790  eqfnun  33798  isbndx  33863  isbnd2  33864  equivbnd2  33873  prdsbnd2  33876  elghomlem2OLD  33967  isdrngo3  34040  riotaclbgBAD  34712  lssatle  34774  opcon3b  34955  cdlemk33N  36668  cdlemk34  36669  wepwsolem  38083  rp-fakeimass  38328  cnvssb  38363  intimag  38419  sscon34b  38788  ntrneiiso  38860  pm11.71  39068  pm14.122b  39095  pm14.123b  39098  iotavalb  39102  eliuniin  39747  eliuniin2  39771  climreeq  40317  rexrsb  41644  reuan  41655  afv0nbfvbi  41706  dfafn5b  41716  elfz2z  41804  zeo2ALTV  42061  nnlog2ge0lt1  42839
  Copyright terms: Public domain W3C validator