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

Theorem impbid2 204
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  |-  ( ps 
->  ch )
impbid2.2  |-  ( ph  ->  ( ch  ->  ps ) )
Assertion
Ref Expression
impbid2  |-  ( ph  ->  ( ps  <->  ch )
)

Proof of Theorem impbid2
StepHypRef Expression
1 impbid2.2 . . 3  |-  ( ph  ->  ( ch  ->  ps ) )
2 impbid2.1 . . 3  |-  ( ps 
->  ch )
31, 2impbid1 203 . 2  |-  ( ph  ->  ( ch  <->  ps )
)
43bicomd 201 1  |-  ( ph  ->  ( ps  <->  ch )
)
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184
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 185
This theorem is referenced by:  biimt  335  biorf  405  biorfi  407  pm4.72  871  biort  891  bimsc1  929  ax13b  1743  euanOLD  2332  cgsexg  3004  cgsex2g  3005  cgsex4g  3006  elab3gf  3110  abidnf  3127  elsnc2g  3906  difsn  4007  eqsn  4033  prel12  4048  dfnfc2  4108  intmin4  4156  dfiin2g  4202  elpw2g  4454  ord0eln0  4772  ssrel  4927  ssrel2  4929  ssrelrel  4939  releldmb  5073  relelrnb  5074  cnveqb  5292  dmsnopg  5309  relcnvtr  5356  f1ocnvb  5653  ffvresb  5873  soisores  6017  riotaclb  6089  fnoprabg  6190  difex2  6382  dfwe2  6392  ordpwsuc  6425  ordunisuc2  6454  limsssuc  6460  dfom2  6477  relcnvexb  6525  dfsmo2  6807  omord  7006  nneob  7090  pw2f1olem  7414  sucdom  7507  fieq0  7670  hartogslem1  7755  rankr1ag  8008  rankeq0b  8066  fidomtri  8162  fidomtri2  8163  isfin2-2  8487  enfin2i  8489  isfin3-2  8535  isf34lem6  8548  isfin1-2  8553  isfin1-3  8554  isfin7-2  8564  axgroth6  8994  ltsonq  9137  ltexnq  9143  znegclb  10681  rpneg  11019  nltpnft  11137  ngtmnft  11138  xrrebnd  11139  qextlt  11172  qextle  11173  iccneg  11405  fzsn  11499  fz1sbc  11535  fzofzp1b  11624  ceilidz  11690  fleqceilz  11692  hashclb  12127  hashnncl  12133  hashfun  12198  wrdlenfi  12257  reim0b  12607  rexanre  12833  rexuzre  12839  lo1resb  13041  o1resb  13043  dvdsext  13583  pceq0  13936  pc11  13945  pcz  13946  ramtcl  14070  cshwsiun  14125  pospo  15142  oduposb  15305  cnvpsb  15382  tsrlemax  15389  issubg2  15695  issubg4  15699  ghmmhmb  15757  pmtrmvd  15961  mndodcong  16044  issubrg2  16884  lpigen  17337  cyggic  18004  ip2eq  18081  maducoeval2  18445  eltg3  18566  bastop  18585  0top  18587  iscld3  18667  isclo2  18691  cnprest  18892  dfcon2  19022  cmphaushmeo  19372  reghaus  19397  nrmhaus  19398  fbun  19412  fsubbas  19439  ufileu  19491  uffix  19493  txflf  19578  fclsrest  19596  flimfnfcls  19600  ptcmplem2  19624  tgpt1  19687  tgpt0  19688  isngp2  20188  nrgdomn  20251  nmhmcn  20674  iscmet3  20803  limcflf  21355  ply1nzb  21593  coe11  21719  dgreq0  21731  sqf11  22476  sqff1o  22519  lgsabs1  22672  lgsquadlem2  22693  usgrafilem2  23324  cusgrafilem3  23388  elghomlem2  23848  nmobndi  24174  hmopadj2  25344  mdslle1i  25720  mdslle2i  25721  ssrelf  25944  eldmgm  27007  rescon  27134  cvmsval  27154  funsseq  27579  brcolinear  28089  outsideofeu  28161  lineunray  28177  wl-sb5nae  28381  wl-ax11-lem2  28400  heicant  28424  nn0prpw  28516  comppfsc  28577  cover2  28605  eqfnun  28613  isbndx  28679  isbnd2  28680  equivbnd2  28689  prdsbnd2  28692  isdrngo3  28763  ceqsex3OLD  29003  wepwsolem  29392  pm11.71  29648  pm14.122b  29675  pm14.123b  29678  iotavalb  29682  climreeq  29784  rexrsb  29991  reuan  30002  afv0nbfvbi  30055  dfafn5b  30065  elfz2z  30196  iswlkg  30283  wwlkn0s  30337  el2wlksoton  30395  el2spthsoton  30396  isclwlkg  30418  vdiscusgra  30535  bnj1173  31991  bj-19.3t  32186  bj-sb3b  32323  bj-sngltag  32474  bj-inftyexpiinj  32530  riotaclbgBAD  32603  riotaclbBAD  32604  lssatle  32658  opcon3b  32839  cdlemk33N  34551  cdlemk34  34552
  Copyright terms: Public domain W3C validator