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

Theorem impbida 830
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 434 . 2  |-  ( ph  ->  ( ps  ->  ch ) )
3 impbida.2 . . 3  |-  ( (
ph  /\  ch )  ->  ps )
43ex 434 . 2  |-  ( ph  ->  ( ch  ->  ps ) )
52, 4impbid 191 1  |-  ( ph  ->  ( ps  <->  ch )
)
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184    /\ wa 369
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This theorem depends on definitions:  df-bi 185  df-an 371
This theorem is referenced by:  eqrdav  2465  eqrdavOLD  2466  frsn  5070  funfvbrb  5994  iinpreima  6011  fnprb  6119  fnprOLD  6120  nvocnv  6175  f1ocnv2d  6510  el2xptp0  6828  1stconst  6871  2ndconst  6872  cnvf1o  6882  tfrlem15  7061  oeeui  7251  ersymb  7325  swoer  7339  erth  7356  boxriin  7511  boxcutc  7512  domunsncan  7617  pw2f1olem  7621  enen1  7657  enen2  7658  domen1  7659  domen2  7660  sdomen1  7661  sdomen2  7662  xpmapenlem  7684  ordiso2  7940  wdomen1  8002  wdomen2  8003  fin23lem26  8705  fpwwe2lem8  9015  r1wunlim  9115  ixxun  11545  xov1plusxeqvd  11666  fzsplit2  11710  fseq1p1m1  11752  elfz2nn0  11768  flflp1  11912  modsubdir  12023  zesq  12257  hashprg  12428  hashgt0elexb  12433  hashbclem  12467  rereb  12916  rlimclim  13332  iserex  13442  caucvgb  13465  mptfzshft  13556  fsumrev  13557  climcnds  13626  dvdsadd2b  13887  bitsfzo  13944  dvdsmulgcd  14051  qden1elz  14149  mrcidb  14870  mrieqvlemd  14884  isacs2  14908  ssclem  15049  issubc3  15076  ffthiso  15156  fuciso  15202  setcmon  15272  setcepi  15273  setcinv  15275  catciso  15292  acsfiindd  15664  issubmnd  15767  mhmf1o  15795  subsubm  15807  resmhm2b  15811  grpinvid1  15908  grpinvid2  15909  subsubg  16029  ssnmz  16048  ghmf1  16100  ghmf1o  16101  conjnmzb  16106  subggim  16119  gicsubgen  16131  gass  16144  odf1  16390  gex1  16417  fislw  16451  sylow3lem2  16454  sylow3lem6  16458  lsmdisj2a  16511  lsmdisj2b  16512  efgred2  16577  dmdprdsplit  16898  0unit  17130  irrednegb  17161  rhmf1o  17181  kerf1hrm  17192  isdrng2  17206  subrgunit  17247  issubdrg  17254  subsubrg  17255  islss3  17405  islss4  17408  lspsnel6  17440  lspsneq0b  17459  islmhm2  17484  lmhmf1o  17492  reslmhm2b  17500  lssvs0or  17556  lvecinv  17559  lspsnel4  17570  lspdisjb  17572  islbs2  17600  islbs3  17601  issubassa  17772  issubassa2  17793  gsumbagdiag  17827  subrgasclcl  17963  prmirredlem  18318  prmirredlemOLD  18321  islindf3  18656  lindsmm  18658  lsslindf  18660  lsslinds  18661  matunit  18975  slesolinvbi  18978  en2top  19281  elcls  19368  neindisj2  19418  neiptopnei  19427  neiptopreu  19428  maxlp  19442  neitr  19475  iscncl  19564  cncnp  19575  isreg2  19672  dis2ndc  19755  1stccnp  19757  islly2  19779  dislly  19792  kgencmp2  19810  pt1hmeo  20070  xkocnv  20078  t0kq  20082  uffixfr  20187  flimcf  20246  cnpflf2  20264  fclscf  20289  cnextf  20329  utopsnneiplem  20513  isucn2  20545  cfilucfilOLD  20835  cfilucfil  20836  metutopOLD  20848  psmetutop  20849  restmetu  20853  tngngp2  20929  tngngp  20931  nmoleub  21001  metdseq0  21121  cnheibor  21218  pcophtb  21292  nmoleub2lem  21360  lmmbr  21460  iscfil3  21475  cmetss  21516  cldcss  21619  mbfeqalem  21812  mbfposb  21823  itg2const2  21911  itgss3  21984  plyco0  22352  dgrlt  22425  ulm2  22542  coseq00topi  22656  coseq0negpitopi  22657  sineq0  22675  atans2  23018  xrlimcnp  23054  dchrelbas2  23268  dchrn0  23281  2sqb  23409  istrkg2ld  23614  tgcgreqb  23628  tgbtwncomb  23636  trgcgrg  23662  legov  23727  legov2  23728  legov3  23739  tglineelsb2  23754  tglinecom  23757  colline  23771  mirinv  23788  mirbtwnb  23793  perpcom  23826  isperp2  23828  lmieu  23855  nb3graprlem1  24155  eleclclwwlknlem2  24522  clwwlknscsh  24523  el2spthonot0  24575  numclwwlk2lem1  24807  grpoinvid1  24936  grpoinvid2  24937  ismndo1  25050  leopmul  26757  hst1h  26850  disjabrex  27144  disjabrexf  27145  disjunsn  27154  erbr3b  27169  f1o3d  27172  funimass4f  27175  fgreu  27213  fcnvgreu  27214  mul2lt0bi  27265  fzsplit3  27295  eliccioo  27323  ogrpinv0le  27396  ogrpaddltbi  27399  ogrpaddltrbid  27401  ogrpinv0lt  27403  isarchi3  27421  fimaproj  27527  metider  27537  qqhval2  27627  qtophaus  27665  aean  27884  imambfm  27901  eulerpartlemgvv  27983  orvcgteel  28074  orvclteel  28079  ballotlemsf1o  28120  sgn3da  28148  sgnnbi  28152  sgnpbi  28153  sgnmulsgn  28156  sgnmulsgp  28157  sconpi1  28352  fprodshft  28711  fprodrev  28712  brofs2  29332  brifs2  29333  broutsideof2  29377  ltflcei  29648  ismblfin  29660  cnambfre  29668  ftc1anclem6  29700  isdrngo2  29992  mrefg2  30271  mzpmfp  30311  mzpmfpOLD  30312  lzenom  30335  elpell14qr2  30430  elpell1qr2  30440  pellfund14b  30467  congabseq  30544  acongeq  30553  jm2.23  30570  jm2.20nn  30571  jm2.25lem1  30572  wepwsolem  30619  islssfg2  30649  lnmlmic  30666  dfacbasgrp  30689  lcmgcdeq  30844  rfcnpre3  31014  rfcnpre4  31015  eliccelioc  31153  fourierdlem48  31483  fourierdlem49  31484  fourierdlem71  31506  lshpnelb  33799  lshpnel2N  33800  lsatspn0  33815  lsatelbN  33821  lsat0cv  33848  lcvexch  33854  lcv1  33856  lkrshp3  33921  lkrpssN  33978  lkrss2N  33984  cvlsupr2  34158  atcvrlln  34334  llncvrlpln  34372  2llnmj  34374  lplncvrlvol  34430  2lplnmj  34436  polcon2bN  34734  pcl0bN  34737  lhpmcvr3  34839  lhpmatb  34845  ltrncoidN  34942  ltrneq3  35022  ltrniotavalbN  35398  cdlemg1cN  35401  diclspsn  36009  dihopelvalcpre  36063  dihord4  36073  dihord  36079  dihmeetlem4preN  36121  dih1dimatlem0  36143  dochsscl  36183  dochoccl  36184  dochord  36185  dochsat  36198  dochshpncl  36199  dochsatshpb  36267  dochshpsat  36269  mapdval4N  36447  mapdsn  36456  hdmap14lem12  36697  hdmapip0  36733  hlhillcs  36776
  Copyright terms: Public domain W3C validator