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

Theorem impbida 828
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  2452  eqrdavOLD  2453  frsn  5016  funfvbrb  5924  iinpreima  5941  fnprb  6044  fnprOLD  6045  nvocnv  6096  f1ocnv2d  6420  1stconst  6770  2ndconst  6771  cnvf1o  6780  tfrlem15  6960  oeeui  7150  ersymb  7224  swoer  7238  erth  7254  boxriin  7414  boxcutc  7415  domunsncan  7520  pw2f1olem  7524  enen1  7560  enen2  7561  domen1  7562  domen2  7563  sdomen1  7564  sdomen2  7565  xpmapenlem  7587  ordiso2  7839  wdomen1  7901  wdomen2  7902  fin23lem26  8604  fpwwe2lem8  8914  r1wunlim  9014  ixxun  11426  xov1plusxeqvd  11547  fzsplit2  11590  elfz2nn0  11596  fseq1p1m1  11650  modsubdir  11883  zesq  12103  hashprg  12272  hashgt0elexb  12277  hashbclem  12322  rereb  12726  rlimclim  13141  iserex  13251  caucvgb  13274  mptfzshft  13362  fsumrev  13363  climcnds  13431  dvdsadd2b  13692  bitsfzo  13748  dvdsmulgcd  13855  qden1elz  13952  mrcidb  14671  mrieqvlemd  14685  isacs2  14709  ssclem  14850  issubc3  14877  ffthiso  14957  fuciso  15003  setcmon  15073  setcepi  15074  setcinv  15076  catciso  15093  acsfiindd  15465  issubmnd  15567  mhmf1o  15591  subsubm  15603  resmhm2b  15607  grpinvid1  15704  grpinvid2  15705  subsubg  15822  ssnmz  15841  ghmf1  15893  ghmf1o  15894  conjnmzb  15899  subggim  15912  gicsubgen  15924  gass  15937  odf1  16183  gex1  16210  fislw  16244  sylow3lem2  16247  sylow3lem6  16251  lsmdisj2a  16304  lsmdisj2b  16305  efgred2  16370  dmdprdsplit  16667  0unit  16894  irrednegb  16925  rhmf1o  16943  kerf1hrm  16953  isdrng2  16964  subrgunit  17005  issubdrg  17012  subsubrg  17013  islss3  17162  islss4  17165  lspsnel6  17197  lspsneq0b  17216  islmhm2  17241  lmhmf1o  17249  reslmhm2b  17257  lssvs0or  17313  lvecinv  17316  lspsnel4  17327  lspdisjb  17329  islbs2  17357  islbs3  17358  issubassa  17517  issubassa2  17537  gsumbagdiag  17568  subrgasclcl  17704  prmirredlem  18041  prmirredlemOLD  18044  islindf3  18379  lindsmm  18381  lsslindf  18383  lsslinds  18384  matunit  18615  slesolinvbi  18618  en2top  18721  elcls  18808  neindisj2  18858  neiptopnei  18867  neiptopreu  18868  maxlp  18882  neitr  18915  iscncl  19004  cncnp  19015  isreg2  19112  dis2ndc  19195  1stccnp  19197  islly2  19219  dislly  19232  kgencmp2  19250  pt1hmeo  19510  xkocnv  19518  t0kq  19522  uffixfr  19627  flimcf  19686  cnpflf2  19704  fclscf  19729  cnextf  19769  utopsnneiplem  19953  isucn2  19985  cfilucfilOLD  20275  cfilucfil  20276  metutopOLD  20288  psmetutop  20289  restmetu  20293  tngngp2  20369  tngngp  20371  nmoleub  20441  metdseq0  20561  cnheibor  20658  pcophtb  20732  nmoleub2lem  20800  lmmbr  20900  iscfil3  20915  cmetss  20956  cldcss  21059  mbfeqalem  21252  mbfposb  21263  itg2const2  21351  itgss3  21424  plyco0  21792  dgrlt  21865  ulm2  21982  coseq00topi  22096  coseq0negpitopi  22097  sineq0  22115  atans2  22458  xrlimcnp  22494  dchrelbas2  22708  dchrn0  22721  2sqb  22849  istrkg2ld  23054  tgcgreqb  23068  tgbtwncomb  23076  trgcgrg  23102  legov  23153  legov2  23154  tglineelsb2  23176  tglinecom  23179  colline  23193  mirinv  23212  mirbtwnb  23217  perpcom  23248  isperp2  23250  nb3graprlem1  23510  grpoinvid1  23868  grpoinvid2  23869  ismndo1  23982  leopmul  25689  hst1h  25782  disjabrex  26076  disjabrexf  26077  disjunsn  26086  f1o3d  26098  funimass4f  26101  fgreu  26140  fcnvgreu  26141  mul2lt0bi  26192  fzsplit3  26222  eliccioo  26250  ogrpinv0le  26323  ogrpaddltbi  26326  ogrpaddltrbid  26328  ogrpinv0lt  26330  isarchi3  26348  metider  26465  qqhval2  26555  aean  26803  imambfm  26820  eulerpartlemgvv  26902  orvcgteel  26993  orvclteel  26998  ballotlemsf1o  27039  sgn3da  27067  sgnnbi  27071  sgnpbi  27072  sgnmulsgn  27075  sgnmulsgp  27076  sconpi1  27271  fprodshft  27630  fprodrev  27631  brofs2  28251  brifs2  28252  broutsideof2  28296  ltflcei  28566  lxflflp1  28568  ismblfin  28579  cnambfre  28587  ftc1anclem6  28619  isdrngo2  28911  mrefg2  29190  mzpmfp  29230  mzpmfpOLD  29231  lzenom  29255  elpell14qr2  29350  elpell1qr2  29360  pellfund14b  29387  congabseq  29464  acongeq  29473  jm2.23  29492  jm2.20nn  29493  jm2.25lem1  29494  wepwsolem  29541  islssfg2  29571  lnmlmic  29588  dfacbasgrp  29611  rfcnpre3  29902  rfcnpre4  29903  el2xptp0  30274  el2spthonot0  30537  eleclclwwlknlem2  30638  Lemma2  30640  numclwwlk2lem1  30842  lshpnelb  32952  lshpnel2N  32953  lsatspn0  32968  lsatelbN  32974  lsat0cv  33001  lcvexch  33007  lcv1  33009  lkrshp3  33074  lkrpssN  33131  lkrss2N  33137  cvlsupr2  33311  atcvrlln  33487  llncvrlpln  33525  2llnmj  33527  lplncvrlvol  33583  2lplnmj  33589  polcon2bN  33887  pcl0bN  33890  lhpmcvr3  33992  lhpmatb  33998  ltrncoidN  34095  ltrneq3  34175  ltrniotavalbN  34551  cdlemg1cN  34554  diclspsn  35162  dihopelvalcpre  35216  dihord4  35226  dihord  35232  dihmeetlem4preN  35274  dih1dimatlem0  35296  dochsscl  35336  dochoccl  35337  dochord  35338  dochsat  35351  dochshpncl  35352  dochsatshpb  35420  dochshpsat  35422  mapdval4N  35600  mapdsn  35609  hdmap14lem12  35850  hdmapip0  35886  hlhillcs  35929
  Copyright terms: Public domain W3C validator