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

Theorem impbida 840
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 435 . 2  |-  ( ph  ->  ( ps  ->  ch ) )
3 impbida.2 . . 3  |-  ( (
ph  /\  ch )  ->  ps )
43ex 435 . 2  |-  ( ph  ->  ( ch  ->  ps ) )
52, 4impbid 193 1  |-  ( ph  ->  ( ps  <->  ch )
)
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 187    /\ wa 370
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 188  df-an 372
This theorem is referenced by:  eqrdav  2418  eqrdavOLD  2419  frsn  4916  funfvbrb  6001  iinpreima  6016  fnprb  6129  fpr2g  6131  nvocnv  6186  fsnex  6187  f1prex  6188  f1ocnv2d  6525  el2xptp0  6842  1stconst  6886  2ndconst  6887  cnvf1o  6897  tfrlem15  7109  oeeui  7302  ersymb  7376  swoer  7390  erth  7407  boxriin  7563  boxcutc  7564  domunsncan  7669  pw2f1olem  7673  enen1  7709  enen2  7710  domen1  7711  domen2  7712  sdomen1  7713  sdomen2  7714  xpmapenlem  7736  ordiso2  8021  wdomen1  8082  wdomen2  8083  fin23lem26  8744  fpwwe2lem8  9051  r1wunlim  9151  mul2lt0bi  11391  ixxun  11640  xov1plusxeqvd  11765  fzsplit2  11811  fseq1p1m1  11855  elfz2nn0  11872  flflp1  12029  modsubdir  12144  zesq  12381  hashprg  12558  hashgt0elexb  12565  hashbclem  12599  rereb  13151  rlimclim  13577  iserex  13687  caucvgb  13713  mptfzshft  13806  fsumrev  13807  climcnds  13876  fprodrev  13998  dvdsadd2b  14314  bitsfzo  14372  dvdsmulgcd  14482  lcmgcdeq  14537  qden1elz  14666  mrcidb  15473  mrieqvlemd  15487  isacs2  15511  cicer  15663  ssclem  15676  issubc3  15706  ffthiso  15786  fuciso  15832  setcmon  15934  setcepi  15935  setcinv  15937  catciso  15954  acsfiindd  16375  issubmnd  16516  mhmf1o  16544  subsubm  16556  resmhm2b  16560  grpinvid1  16666  grpinvid2  16667  subsubg  16792  ssnmz  16811  ghmf1  16863  ghmf1o  16864  conjnmzb  16869  subggim  16882  gicsubgen  16894  gass  16907  odf1  17154  gex1  17184  fislw  17218  sylow3lem2  17221  sylow3lem6  17225  lsmdisj2a  17278  lsmdisj2b  17279  efgred2  17344  dmdprdsplit  17621  0unit  17849  irrednegb  17880  rhmf1o  17901  kerf1hrm  17912  isdrng2  17926  subrgunit  17967  issubdrg  17974  subsubrg  17975  islss3  18123  islss4  18126  lspsnel6  18158  lspsneq0b  18177  islmhm2  18202  lmhmf1o  18210  reslmhm2b  18218  lssvs0or  18274  lvecinv  18277  lspsnel4  18288  lspdisjb  18290  islbs2  18318  islbs3  18319  issubassa  18489  issubassa2  18510  gsumbagdiag  18541  subrgasclcl  18663  prmirredlem  19001  islindf3  19321  lindsmm  19323  lsslindf  19325  lsslinds  19326  matunit  19640  slesolinvbi  19643  en2top  19938  elcls  20026  neindisj2  20076  neiptopnei  20085  neiptopreu  20086  maxlp  20100  neitr  20133  iscncl  20222  cncnp  20233  isreg2  20330  dis2ndc  20412  1stccnp  20414  islly2  20436  dislly  20449  dissnlocfin  20481  kgencmp2  20498  pt1hmeo  20758  xkocnv  20766  t0kq  20770  uffixfr  20875  flimcf  20934  cnpflf2  20952  fclscf  20977  cnextf  21018  utopsnneiplem  21199  isucn2  21231  cfilucfil  21511  psmetutop  21519  restmetu  21522  tngngp2  21597  tngngp  21599  nmoleub  21673  nmoleubOLD  21689  metdseq0  21808  cnheibor  21905  pcophtb  21979  nmoleub2lem  22047  lmmbr  22147  iscfil3  22162  cmetss  22203  cldcss  22302  mbfeqalem  22505  mbfposb  22516  itg2const2  22606  itgss3  22679  plyco0  23053  dgrlt  23127  ulm2  23244  coseq00topi  23361  coseq0negpitopi  23362  sineq0  23380  relogbcxpb  23628  atans2  23761  xrlimcnp  23798  dchrelbas2  24067  dchrn0  24080  2sqb  24208  istrkg2ld  24410  tgcgreqb  24427  tgbtwncomb  24435  trgcgrg  24461  legov  24529  legov2  24530  legov3  24542  hlbtwn  24555  tglineelsb2  24576  tglinecom  24579  colline  24593  mirinv  24610  mirbtwnb  24615  mirbtwnhl  24623  perpcom  24654  isperp2  24656  oppcom  24682  opphllem3  24687  lnopp2hpgb  24701  colopp  24707  colhp  24708  lmieu  24722  iscgra1  24748  dfcgra2  24766  nb3graprlem1  25065  eleclclwwlknlem2  25432  clwwlknscsh  25433  el2spthonot0  25485  numclwwlk2lem1  25716  grpoinvid1  25844  grpoinvid2  25845  ismndo1  25958  leopmul  27663  hst1h  27756  disjabrex  28072  disjabrexf  28073  erbr3b  28103  elsnxp  28104  f1o3d  28110  funimass4f  28115  fgreu  28155  fcnvgreu  28156  1stpreimas  28167  fcobij  28194  resf1o  28199  fzsplit3  28247  eliccioo  28279  ogrpinv0le  28358  ogrpaddltbi  28361  ogrpaddltrbid  28363  ogrpinv0lt  28365  isarchi3  28383  1smat1  28510  fimaproj  28540  qtophaus  28543  reff  28546  locfinreflem  28547  cmpcref  28557  metider  28577  pstmfval  28579  qqhval2  28666  aean  28947  imambfm  28964  eulerpartlemgvv  29076  orvcgteel  29167  orvclteel  29172  ballotlemsf1o  29213  sgn3da  29241  sgnnbi  29245  sgnpbi  29246  sgnmulsgn  29249  sgnmulsgp  29250  sconpi1  29791  brofs2  30670  brifs2  30671  broutsideof2  30715  ltflcei  31681  poimirlem25  31713  ismblfin  31729  cnambfre  31737  ftc1anclem6  31770  isdrngo2  31945  lshpnelb  32303  lshpnel2N  32304  lsatspn0  32319  lsatelbN  32325  lsat0cv  32352  lcvexch  32358  lcv1  32360  lkrshp3  32425  lkrpssN  32482  lkrss2N  32488  cvlsupr2  32662  atcvrlln  32838  llncvrlpln  32876  2llnmj  32878  lplncvrlvol  32934  2lplnmj  32940  polcon2bN  33238  pcl0bN  33241  lhpmcvr3  33343  lhpmatb  33349  ltrncoidN  33446  ltrneq3  33527  ltrniotavalbN  33904  cdlemg1cN  33907  diclspsn  34515  dihopelvalcpre  34569  dihord4  34579  dihord  34585  dihmeetlem4preN  34627  dih1dimatlem0  34649  dochsscl  34689  dochoccl  34690  dochord  34691  dochsat  34704  dochshpncl  34705  dochsatshpb  34773  dochshpsat  34775  mapdval4N  34953  mapdsn  34962  hdmap14lem12  35203  hdmapip0  35239  hlhillcs  35282  mrefg2  35302  mzpmfp  35342  lzenom  35365  elpell14qr2  35462  elpell1qr2  35472  pellfund14b  35501  congabseq  35578  acongeq  35587  jm2.23  35605  jm2.20nn  35606  jm2.25lem1  35607  wepwsolem  35654  islssfg2  35683  lnmlmic  35700  dfacbasgrp  35721  rfcnpre3  37042  rfcnpre4  37043  ioossioobi  37251  iccshift  37252  iocopn  37254  eliccelioc  37255  iooshift  37256  icoopn  37259  limcdm0  37318  islptre  37319  islpcn  37339  limcresioolb  37344  fperdvper  37410  itgperiod  37475  fourierdlem32  37618  fourierdlem33  37619  fourierdlem48  37634  fourierdlem49  37635  fourierdlem71  37657  fourierdlem81  37667  m1mod0mod1  38170  mgmhmf1o  38602  issubmgm2  38605  subsubmgm  38612  resmgmhm2b  38615  rnghmf1o  38718  rngcinv  38798  rngcinvALTV  38810  ringcinv  38849  ringcinvALTV  38873  nn0ob  39148
  Copyright terms: Public domain W3C validator