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  1405  19.33b  1613  19.9t  1785  19.9tOLD  1867  a16gb  2063  sb4b  2067  eupickbi  2283  euor2  2285  2eu1  2297  2eu3  2299  ceqsalg  2897  undif4  3599  sneqbg  3883  opthpr  3890  elpwuni  4091  ordssun  4595  suc11  4599  unizlim  4612  eusv2i  4634  reusv2lem3  4640  reusv3  4645  reuxfr2d  4660  iunpw  4673  ssonprc  4686  onint0  4690  soltmin  5185  ssxpb  5213  xp11  5214  xpcan  5215  xpcan2  5216  iotanul  5337  imadif  5432  2elresin  5460  mpteqb  5721  f1fveq  5908  f1elima  5909  f1imass  5910  fliftf  5937  sorpssuni  6428  sorpssint  6429  oa00  6699  omcan  6709  omopth2  6724  oecan  6729  nnarcl  6756  iserd  6828  ecopover  6905  map0g  6950  fundmen  7077  fopwdom  7113  onfin  7194  fineqvlem  7220  f1finf1o  7232  isfiniteg  7264  inficl  7325  tc00  7580  cardnueq0  7744  cardsdomel  7754  wdomfil  7835  wdomnumr  7838  alephsucdom  7853  cardalephex  7864  dfac12lem2  7917  cfeq0  8029  fin23lem24  8095  fin1a2lem9  8181  carden  8320  axrepnd  8363  axacndlem4  8379  gchpwdom  8443  gchina  8468  r1tskina  8551  addcanpi  8670  mulcanpi  8671  elnpi  8759  addcan  9143  addcan2  9144  neg11  9245  negreb  9259  add20  9433  mulcand  9548  cru  9885  uz11  10401  eqreznegel  10454  lbzbi  10457  rpnnen1  10498  xrmaxlt  10662  xrltmin  10663  xrmaxle  10664  xrlemin  10665  xneg11  10694  xsubge0  10733  xrub  10783  elioc2  10866  elico2  10867  elicc2  10868  fzopth  10981  flidz  11105  expeq0  11297  sq01  11388  fz1eqb  11524  hash1snb  11568  ccatopth  11663  ccatopth2  11664  cj11  11854  sqr0  11934  abs00  11981  recan  12027  rlimdm  12232  rpnnen2  12712  0dvds  12757  dvds1  12785  alzdvds  12786  gcdeq0  12908  algcvgblem  12955  prmexpb  13004  prmreclem3  13173  4sqlem11  13210  moni  13849  spwex  14548  grprcan  14725  grplcan  14744  grpinv11  14747  galcan  14968  sylow2a  15140  subgdisjb  15212  drngmuleq0  15745  lspsncmp  16079  fidomndrng  16258  coe1tm  16559  xrsdsreclb  16635  znidomb  16732  istps2OLD  16876  tgdom  16933  en1top  16939  cmpfi  17352  txcmpb  17555  hmeocnvb  17682  flimcls  17893  hauspwpwf1  17895  flftg  17904  ghmcnp  18010  metrest  18283  icoopnst  18652  iocopnst  18653  ishl2  19002  vitali  19183  mbfi1fseqlem4  19288  aannenlem1  19923  perfect  20693  usgra1v  21086  grporcan  21320  grpolcan  21332  ip2eqi  21869  hial2eq  22119  eigorthi  22851  stge1i  23252  stle0i  23253  mdbr3  23311  mdbr4  23312  atsseq  23361  mdsymlem7  23423  eqvincg  23470  reuxfr3d  23491  xmulcand  23691  untangtr  24732  tfrALTlem  25102  sltval2  25136  ordtopcon  25705  ordtopt0  25708  filnetlem4  25922  seqpo  26049  fphpd  26490  pellexlem3  26507  qirropth  26584  expdioph  26707  rpnnen3  26716  lmisfree  26903  iotasbc  27210  2reu1  27555  2reu3  27557  rlimdmafv  27633  equs5bAUX7  28946  a16gbNEW7  28958  sb4bNEW7  28964  lshpcmp  29237  lsatcmp  29252  lsatcmp2  29253  ltrneq2  30396  ltrneq  30397  tendospcanN  31272  dochlkr  31634  lcfl7N  31750  hgmap11  32154
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