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

Theorem impbid1 194
Description: Infer an equivalence from two implications. (Contributed by NM, 6-Mar-2007.)
Hypotheses
Ref Expression
impbid1.1  |-  ( ph  ->  ( ps  ->  ch ) )
impbid1.2  |-  ( ch 
->  ps )
Assertion
Ref Expression
impbid1  |-  ( ph  ->  ( ps  <->  ch )
)

Proof of Theorem impbid1
StepHypRef Expression
1 impbid1.1 . 2  |-  ( ph  ->  ( ps  ->  ch ) )
2 impbid1.2 . . 3  |-  ( ch 
->  ps )
32a1i 10 . 2  |-  ( ph  ->  ( ch  ->  ps ) )
41, 3impbid 183 1  |-  ( ph  ->  ( ps  <->  ch )
)
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 176
This theorem is referenced by:  impbid2  195  iba  489  ibar  490  pm5.71  902  cad0  1390  19.33b  1595  19.9t  1782  a16gb  1990  sb4b  1994  eupickbi  2209  euor2  2211  2eu1  2223  2eu3  2225  ceqsalg  2812  undif4  3511  sneqbg  3783  opthpr  3790  elpwuni  3989  ordssun  4492  suc11  4496  unizlim  4509  eusv2i  4531  reusv2lem3  4537  reusv3  4542  reuxfr2d  4557  iunpw  4570  ssonprc  4583  onint0  4587  soltmin  5082  ssxpb  5110  xp11  5111  xpcan  5112  xpcan2  5113  iotanul  5234  imadif  5327  2elresin  5355  mpteqb  5614  f1fveq  5786  f1elima  5787  f1imass  5788  fliftf  5814  sorpssuni  6286  sorpssint  6287  oa00  6557  omcan  6567  omopth2  6582  oecan  6587  nnarcl  6614  iserd  6686  ecopover  6762  map0g  6807  fundmen  6934  fopwdom  6970  onfin  7051  fineqvlem  7077  f1finf1o  7086  isfiniteg  7117  inficl  7178  tc00  7433  cardnueq0  7597  cardsdomel  7607  wdomfil  7688  wdomnumr  7691  alephsucdom  7706  cardalephex  7717  dfac12lem2  7770  cfeq0  7882  fin23lem24  7948  fin1a2lem9  8034  carden  8173  axrepnd  8216  axacndlem4  8232  gchpwdom  8296  gchina  8321  r1tskina  8404  addcanpi  8523  mulcanpi  8524  elnpi  8612  addcan  8996  addcan2  8997  neg11  9098  negreb  9112  add20  9286  mulcand  9401  cru  9738  uz11  10250  eqreznegel  10303  lbzbi  10306  rpnnen1  10347  xrmaxlt  10510  xrltmin  10511  xrmaxle  10512  xrlemin  10513  xneg11  10542  xsubge0  10581  xrub  10630  elioc2  10713  elico2  10714  elicc2  10715  fzopth  10828  flidz  10941  expeq0  11132  sq01  11223  fz1eqb  11348  ccatopth  11462  ccatopth2  11463  cj11  11647  sqr0  11727  abs00  11774  recan  11820  rlimdm  12025  rpnnen2  12504  0dvds  12549  dvds1  12577  alzdvds  12578  gcdeq0  12700  algcvgblem  12747  prmexpb  12796  prmreclem3  12965  4sqlem11  13002  moni  13639  spwex  14338  grprcan  14515  grplcan  14534  grpinv11  14537  galcan  14758  sylow2a  14930  subgdisjb  15002  drngmuleq0  15535  lspsncmp  15869  fidomndrng  16048  coe1tm  16349  xrsdsreclb  16418  znidomb  16515  istps2OLD  16659  tgdom  16716  en1top  16722  cmpfi  17135  txcmpb  17338  hmeocnvb  17465  flimcls  17680  hauspwpwf1  17682  flftg  17691  ghmcnp  17797  metrest  18070  icoopnst  18437  iocopnst  18438  ishl2  18787  vitali  18968  mbfi1fseqlem4  19073  aannenlem1  19708  perfect  20470  grporcan  20888  grpolcan  20900  ip2eqi  21435  hial2eq  21685  eigorthi  22417  stge1i  22818  stle0i  22819  mdbr3  22877  mdbr4  22878  atsseq  22927  mdsymlem7  22989  xmulcand  23104  eqvincg  23130  reuxfr3d  23138  untangtr  24060  tfrALTlem  24276  sltval2  24310  ordtopcon  24878  ordtopt0  24881  oooeqim2  25053  prj1b  25079  prj3  25080  fixpb  25093  eqfnung2  25118  efilcp  25552  addcanrg  25667  filnetlem4  26330  seqpo  26457  fphpd  26899  pellexlem3  26916  qirropth  26993  expdioph  27116  rpnnen3  27125  lmisfree  27312  iotasbc  27619  2reu1  27964  2reu3  27966  usgra1v  28126  lshpcmp  29178  lsatcmp  29193  lsatcmp2  29194  ltrneq2  30337  ltrneq  30338  tendospcanN  31213  dochlkr  31575  lcfl7N  31691  hgmap11  32095
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 177
  Copyright terms: Public domain W3C validator