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

Theorem impbid1 195
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 11 . 2  |-  ( ph  ->  ( ch  ->  ps ) )
41, 3impbid 184 1  |-  ( ph  ->  ( ps  <->  ch )
)
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 177
This theorem is referenced by:  impbid2  196  iba  490  ibar  491  pm5.71  903  cad0  1409  19.33b  1618  19.9t  1793  19.9tOLD  1880  sb4b  2090  a16gb  2134  eupickbi  2346  euor2  2348  2eu1  2360  2eu3  2362  ceqsalg  2967  undif4  3671  sneqbg  3956  opthpr  3963  elpwuni  4165  ordssun  4667  suc11  4671  unizlim  4684  eusv2i  4706  reusv2lem3  4712  reusv3  4717  reuxfr2d  4732  iunpw  4745  ssonprc  4758  onint0  4762  soltmin  5259  ssxpb  5289  xp11  5290  xpcan  5291  xpcan2  5292  iotanul  5419  imadif  5514  2elresin  5542  mpteqb  5805  f1fveq  5994  f1elima  5995  f1imass  5996  fliftf  6023  sorpssuni  6517  sorpssint  6518  oa00  6788  omcan  6798  omopth2  6813  oecan  6818  nnarcl  6845  iserd  6917  ecopover  6994  map0g  7039  fundmen  7166  fopwdom  7202  onfin  7283  fineqvlem  7309  f1finf1o  7321  isfiniteg  7353  inficl  7416  tc00  7671  cardnueq0  7835  cardsdomel  7845  wdomfil  7926  wdomnumr  7929  alephsucdom  7944  cardalephex  7955  dfac12lem2  8008  cfeq0  8120  fin23lem24  8186  fin1a2lem9  8272  carden  8410  axrepnd  8453  axacndlem4  8469  gchpwdom  8533  gchina  8558  r1tskina  8641  addcanpi  8760  mulcanpi  8761  elnpi  8849  addcan  9234  addcan2  9235  neg11  9336  negreb  9350  add20  9524  mulcand  9639  cru  9976  uz11  10492  eqreznegel  10545  lbzbi  10548  rpnnen1  10589  xrmaxlt  10753  xrltmin  10754  xrmaxle  10755  xrlemin  10756  xneg11  10785  xsubge0  10824  xrub  10874  elioc2  10957  elico2  10958  elicc2  10959  fzopth  11073  flidz  11201  expeq0  11393  sq01  11484  fz1eqb  11620  hash1snb  11664  ccatopth  11759  ccatopth2  11760  cj11  11950  sqr0  12030  abs00  12077  recan  12123  rlimdm  12328  rpnnen2  12808  0dvds  12853  dvds1  12881  alzdvds  12882  gcdeq0  13004  algcvgblem  13051  prmexpb  13100  prmreclem3  13269  4sqlem11  13306  moni  13945  spwex  14644  grprcan  14821  grplcan  14840  grpinv11  14843  galcan  15064  sylow2a  15236  subgdisjb  15308  drngmuleq0  15841  lspsncmp  16171  fidomndrng  16350  coe1tm  16648  xrsdsreclb  16728  znidomb  16825  istps2OLD  16969  tgdom  17026  en1top  17032  cmpfi  17454  txcmpb  17659  hmeocnvb  17789  flimcls  18000  hauspwpwf1  18002  flftg  18011  ghmcnp  18127  metrest  18537  icoopnst  18947  iocopnst  18948  ishl2  19307  vitali  19488  mbfi1fseqlem4  19593  aannenlem1  20228  perfect  20998  usgra1v  21392  is2wlk  21548  grporcan  21792  grpolcan  21804  ip2eqi  22341  hial2eq  22591  eigorthi  23323  stge1i  23724  stle0i  23725  mdbr3  23783  mdbr4  23784  atsseq  23833  mdsymlem7  23895  eqvincg  23944  reuxfr3d  23959  xmulcand  24150  untangtr  25146  tfrALTlem  25526  sltval2  25560  ordtopcon  26132  ordtopt0  26135  filnetlem4  26342  seqpo  26383  fphpd  26809  pellexlem3  26826  qirropth  26903  expdioph  27026  rpnnen3  27035  lmisfree  27222  iotasbc  27529  2reu1  27873  2reu3  27875  rlimdmafv  27950  usgra2pthspth  28077  usgra2wlkspth  28080  usg2wotspth  28123  usg2spot2nb  28210  equs5bAUX7  29285  a16gbNEW7  29297  sb4bNEW7  29303  lshpcmp  29517  lsatcmp  29532  lsatcmp2  29533  ltrneq2  30676  ltrneq  30677  tendospcanN  31552  dochlkr  31914  lcfl7N  32030  hgmap11  32434
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 178
  Copyright terms: Public domain W3C validator