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

Theorem impbida 806
Description: Deduce an equivalence from two implications. (Contributed by NM, 17-Feb-2007.)
Hypotheses
Ref Expression
impbida.1  |-  ( (
ph  /\  ps )  ->  ch )
impbida.2  |-  ( (
ph  /\  ch )  ->  ps )
Assertion
Ref Expression
impbida  |-  ( ph  ->  ( ps  <->  ch )
)

Proof of Theorem impbida
StepHypRef Expression
1 impbida.1 . . 3  |-  ( (
ph  /\  ps )  ->  ch )
21ex 424 . 2  |-  ( ph  ->  ( ps  ->  ch ) )
3 impbida.2 . . 3  |-  ( (
ph  /\  ch )  ->  ps )
43ex 424 . 2  |-  ( ph  ->  ( ch  ->  ps ) )
52, 4impbid 184 1  |-  ( ph  ->  ( ps  <->  ch )
)
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 177    /\ wa 359
This theorem is referenced by:  eqrdav  2403  frsn  4907  funfvbrb  5802  iinpreima  5819  fnpr  5909  fnprOLD  5910  f1ocnv2d  6254  1stconst  6394  2ndconst  6395  cnvf1o  6404  tfrlem15  6612  oeeui  6804  ersymb  6878  swoer  6892  erth  6908  boxriin  7063  boxcutc  7064  domunsncan  7167  pw2f1olem  7171  enen1  7206  enen2  7207  domen1  7208  domen2  7209  sdomen1  7210  sdomen2  7211  xpmapenlem  7233  ordiso2  7440  wdomen1  7500  wdomen2  7501  fin23lem26  8161  fpwwe2lem8  8468  r1wunlim  8568  ixxun  10888  xov1plusxeqvd  10997  fzsplit2  11032  elfz2nn0  11038  fseq1p1m1  11077  modsubdir  11240  zesq  11457  hashprg  11621  hashgt0elexb  11626  hashbclem  11656  rereb  11880  rlimclim  12295  iserex  12405  caucvgb  12428  fsumrev  12517  fsumshft  12518  climcnds  12586  dvdsadd2b  12847  bitsfzo  12902  dvdsmulgcd  13009  qden1elz  13104  mrcidb  13795  mrieqvlemd  13809  isacs2  13833  ssclem  13974  issubc3  14001  ffthiso  14081  fuciso  14127  setcmon  14197  setcepi  14198  setcinv  14200  catciso  14217  acsfiindd  14558  issubmnd  14679  subsubm  14712  resmhm2b  14716  grpinvid1  14808  grpinvid2  14809  subsubg  14918  ssnmz  14937  ghmf1  14989  ghmf1o  14990  conjnmzb  14995  subggim  15008  gicsubgen  15020  gass  15033  odf1  15153  gex1  15180  fislw  15214  sylow3lem2  15217  sylow3lem6  15221  lsmdisj2a  15274  lsmdisj2b  15275  efgred2  15340  dmdprdsplit  15560  0unit  15740  irrednegb  15771  isdrng2  15800  subrgunit  15841  issubdrg  15848  subsubrg  15849  islss3  15990  islss4  15993  lspsnel6  16025  lspsneq0b  16044  islmhm2  16069  lmhmf1o  16077  reslmhm2b  16085  lssvs0or  16137  lvecinv  16140  lspsnel4  16151  lspdisjb  16153  islbs2  16181  islbs3  16182  issubassa  16338  issubassa2  16358  gsumbagdiag  16396  subrgasclcl  16514  prmirredlem  16728  en2top  17005  elcls  17092  neindisj2  17142  neiptopnei  17151  neiptopreu  17152  maxlp  17165  neitr  17198  iscncl  17287  cncnp  17298  isreg2  17395  dis2ndc  17476  1stccnp  17478  islly2  17500  dislly  17513  kgencmp2  17531  pt1hmeo  17791  xkocnv  17799  t0kq  17803  uffixfr  17908  flimcf  17967  cnpflf2  17985  fclscf  18010  cnextf  18050  utopsnneiplem  18230  isucn2  18262  cfilucfilOLD  18552  cfilucfil  18553  metutopOLD  18565  psmetutop  18566  restmetu  18570  tngngp2  18646  tngngp  18648  nmoleub  18718  metdseq0  18837  cnheibor  18933  pcophtb  19007  nmoleub2lem  19075  lmmbr  19164  iscfil3  19179  cmetss  19220  cldcss  19295  mbfeqalem  19487  mbfposb  19498  itg2const2  19586  itgss3  19659  plyco0  20064  dgrlt  20137  ulm2  20254  coseq00topi  20363  coseq0negpitopi  20364  sineq0  20382  atans2  20724  xrlimcnp  20760  dchrelbas2  20974  dchrn0  20987  2sqb  21115  nb3graprlem1  21413  grpoinvid1  21771  grpoinvid2  21772  ismndo1  21885  leopmul  23590  hst1h  23683  disjabrex  23977  disjabrexf  23978  f1o3d  23994  funimass4f  23997  fzsplit3  24103  eliccioo  24130  kerf1hrm  24215  metider  24242  qqhval2  24319  aean  24548  imambfm  24565  orvcgteel  24678  orvclteel  24683  ballotlemsf1o  24724  sconpi1  24879  fprodshft  25253  fprodrev  25254  brofs2  25915  brifs2  25916  broutsideof2  25960  ltflcei  26140  lxflflp1  26142  ismblfin  26146  cnambfre  26154  isdrngo2  26464  mrefg2  26651  mzpmfp  26694  lzenom  26718  elpell14qr2  26815  elpell1qr2  26825  pellfund14b  26852  congabseq  26929  acongeq  26938  jm2.23  26957  jm2.20nn  26958  jm2.25lem1  26959  wepwsolem  27006  islssfg2  27037  lnmlmic  27054  dfacbasgrp  27141  islindf3  27164  lindsmm  27166  lsslindf  27168  lsslinds  27169  rfcnpre3  27571  rfcnpre4  27572  el2xptp0  27949  el2spthonot0  28068  lshpnelb  29467  lshpnel2N  29468  lsatspn0  29483  lsatelbN  29489  lsat0cv  29516  lcvexch  29522  lcv1  29524  lkrshp3  29589  lkrpssN  29646  lkrss2N  29652  cvlsupr2  29826  atcvrlln  30002  llncvrlpln  30040  2llnmj  30042  lplncvrlvol  30098  2lplnmj  30104  polcon2bN  30402  pcl0bN  30405  lhpmcvr3  30507  lhpmatb  30513  ltrncoidN  30610  ltrneq3  30690  ltrniotavalbN  31066  cdlemg1cN  31069  diclspsn  31677  dihopelvalcpre  31731  dihord4  31741  dihord  31747  dihmeetlem4preN  31789  dih1dimatlem0  31811  dochsscl  31851  dochoccl  31852  dochord  31853  dochsat  31866  dochshpncl  31867  dochsatshpb  31935  dochshpsat  31937  mapdval4N  32115  mapdsn  32124  hdmap14lem12  32365  hdmapip0  32401  hlhillcs  32444
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  df-an 361
  Copyright terms: Public domain W3C validator