MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  impbida Structured version   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  2435  frsn  4948  funfvbrb  5843  iinpreima  5860  fnpr  5950  fnprOLD  5951  f1ocnv2d  6295  1stconst  6435  2ndconst  6436  cnvf1o  6445  tfrlem15  6653  oeeui  6845  ersymb  6919  swoer  6933  erth  6949  boxriin  7104  boxcutc  7105  domunsncan  7208  pw2f1olem  7212  enen1  7247  enen2  7248  domen1  7249  domen2  7250  sdomen1  7251  sdomen2  7252  xpmapenlem  7274  ordiso2  7484  wdomen1  7544  wdomen2  7545  fin23lem26  8205  fpwwe2lem8  8512  r1wunlim  8612  ixxun  10932  xov1plusxeqvd  11041  fzsplit2  11076  elfz2nn0  11082  fseq1p1m1  11122  modsubdir  11285  zesq  11502  hashprg  11666  hashgt0elexb  11671  hashbclem  11701  rereb  11925  rlimclim  12340  iserex  12450  caucvgb  12473  fsumrev  12562  fsumshft  12563  climcnds  12631  dvdsadd2b  12892  bitsfzo  12947  dvdsmulgcd  13054  qden1elz  13149  mrcidb  13840  mrieqvlemd  13854  isacs2  13878  ssclem  14019  issubc3  14046  ffthiso  14126  fuciso  14172  setcmon  14242  setcepi  14243  setcinv  14245  catciso  14262  acsfiindd  14603  issubmnd  14724  subsubm  14757  resmhm2b  14761  grpinvid1  14853  grpinvid2  14854  subsubg  14963  ssnmz  14982  ghmf1  15034  ghmf1o  15035  conjnmzb  15040  subggim  15053  gicsubgen  15065  gass  15078  odf1  15198  gex1  15225  fislw  15259  sylow3lem2  15262  sylow3lem6  15266  lsmdisj2a  15319  lsmdisj2b  15320  efgred2  15385  dmdprdsplit  15605  0unit  15785  irrednegb  15816  isdrng2  15845  subrgunit  15886  issubdrg  15893  subsubrg  15894  islss3  16035  islss4  16038  lspsnel6  16070  lspsneq0b  16089  islmhm2  16114  lmhmf1o  16122  reslmhm2b  16130  lssvs0or  16182  lvecinv  16185  lspsnel4  16196  lspdisjb  16198  islbs2  16226  islbs3  16227  issubassa  16383  issubassa2  16403  gsumbagdiag  16441  subrgasclcl  16559  prmirredlem  16773  en2top  17050  elcls  17137  neindisj2  17187  neiptopnei  17196  neiptopreu  17197  maxlp  17211  neitr  17244  iscncl  17333  cncnp  17344  isreg2  17441  dis2ndc  17523  1stccnp  17525  islly2  17547  dislly  17560  kgencmp2  17578  pt1hmeo  17838  xkocnv  17846  t0kq  17850  uffixfr  17955  flimcf  18014  cnpflf2  18032  fclscf  18057  cnextf  18097  utopsnneiplem  18277  isucn2  18309  cfilucfilOLD  18599  cfilucfil  18600  metutopOLD  18612  psmetutop  18613  restmetu  18617  tngngp2  18693  tngngp  18695  nmoleub  18765  metdseq0  18884  cnheibor  18980  pcophtb  19054  nmoleub2lem  19122  lmmbr  19211  iscfil3  19226  cmetss  19267  cldcss  19342  mbfeqalem  19534  mbfposb  19545  itg2const2  19633  itgss3  19706  plyco0  20111  dgrlt  20184  ulm2  20301  coseq00topi  20410  coseq0negpitopi  20411  sineq0  20429  atans2  20771  xrlimcnp  20807  dchrelbas2  21021  dchrn0  21034  2sqb  21162  nb3graprlem1  21460  grpoinvid1  21818  grpoinvid2  21819  ismndo1  21932  leopmul  23637  hst1h  23730  disjabrex  24024  disjabrexf  24025  f1o3d  24041  funimass4f  24044  fzsplit3  24150  eliccioo  24177  kerf1hrm  24262  metider  24289  qqhval2  24366  aean  24595  imambfm  24612  orvcgteel  24725  orvclteel  24730  ballotlemsf1o  24771  sconpi1  24926  fprodshft  25300  fprodrev  25301  brofs2  26011  brifs2  26012  broutsideof2  26056  ltflcei  26239  lxflflp1  26241  ismblfin  26247  cnambfre  26255  ftc1anclem6  26285  isdrngo2  26574  mrefg2  26761  mzpmfp  26804  lzenom  26828  elpell14qr2  26925  elpell1qr2  26935  pellfund14b  26962  congabseq  27039  acongeq  27048  jm2.23  27067  jm2.20nn  27068  jm2.25lem1  27069  wepwsolem  27116  islssfg2  27146  lnmlmic  27163  dfacbasgrp  27250  islindf3  27273  lindsmm  27275  lsslindf  27277  lsslinds  27278  rfcnpre3  27680  rfcnpre4  27681  el2xptp0  28061  el2spthonot0  28338  lshpnelb  29782  lshpnel2N  29783  lsatspn0  29798  lsatelbN  29804  lsat0cv  29831  lcvexch  29837  lcv1  29839  lkrshp3  29904  lkrpssN  29961  lkrss2N  29967  cvlsupr2  30141  atcvrlln  30317  llncvrlpln  30355  2llnmj  30357  lplncvrlvol  30413  2lplnmj  30419  polcon2bN  30717  pcl0bN  30720  lhpmcvr3  30822  lhpmatb  30828  ltrncoidN  30925  ltrneq3  31005  ltrniotavalbN  31381  cdlemg1cN  31384  diclspsn  31992  dihopelvalcpre  32046  dihord4  32056  dihord  32062  dihmeetlem4preN  32104  dih1dimatlem0  32126  dochsscl  32166  dochoccl  32167  dochord  32168  dochsat  32181  dochshpncl  32182  dochsatshpb  32250  dochshpsat  32252  mapdval4N  32430  mapdsn  32439  hdmap14lem12  32680  hdmapip0  32716  hlhillcs  32759
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