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

Theorem impbida 805
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 423 . 2  |-  ( ph  ->  ( ps  ->  ch ) )
3 impbida.2 . . 3  |-  ( (
ph  /\  ch )  ->  ps )
43ex 423 . 2  |-  ( ph  ->  ( ch  ->  ps ) )
52, 4impbid 183 1  |-  ( ph  ->  ( ps  <->  ch )
)
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 176    /\ wa 358
This theorem is referenced by:  eqrdav  2282  frsn  4760  funfvbrb  5638  iinpreima  5655  f1ocnv2d  6068  1stconst  6207  2ndconst  6208  cnvf1o  6217  tfrlem15  6408  oeeui  6600  ersymb  6674  swoer  6688  erth  6704  boxriin  6858  boxcutc  6859  domunsncan  6962  pw2f1olem  6966  enen1  7001  enen2  7002  domen1  7003  domen2  7004  sdomen1  7005  sdomen2  7006  xpmapenlem  7028  ordiso2  7230  wdomen1  7290  wdomen2  7291  fin23lem26  7951  fpwwe2lem8  8259  r1wunlim  8359  ixxun  10672  xov1plusxeqvd  10780  fzsplit2  10815  elfz2nn0  10821  fseq1p1m1  10857  modsubdir  11008  zesq  11224  hashprg  11368  hashbclem  11390  rereb  11605  rlimclim  12020  iserex  12130  caucvgb  12152  fsumrev  12241  fsumshft  12242  climcnds  12310  dvdsadd2b  12571  bitsfzo  12626  dvdsmulgcd  12733  qden1elz  12828  mrcidb  13517  mrieqvlemd  13531  isacs2  13555  ssclem  13696  issubc3  13723  ffthiso  13803  fuciso  13849  setcmon  13919  setcepi  13920  setcinv  13922  catciso  13939  acsfiindd  14280  issubmnd  14401  subsubm  14434  resmhm2b  14438  grpinvid1  14530  grpinvid2  14531  subsubg  14640  ssnmz  14659  ghmf1  14711  ghmf1o  14712  conjnmzb  14717  subggim  14730  gicsubgen  14742  gass  14755  odf1  14875  gex1  14902  fislw  14936  sylow3lem2  14939  sylow3lem6  14943  lsmdisj2a  14996  lsmdisj2b  14997  efgred2  15062  dmdprdsplit  15282  0unit  15462  irrednegb  15493  isdrng2  15522  subrgunit  15563  issubdrg  15570  subsubrg  15571  islss3  15716  islss4  15719  lspsnel6  15751  lspsneq0b  15770  islmhm2  15795  lmhmf1o  15803  reslmhm2b  15811  lssvs0or  15863  lvecinv  15866  lspsnel4  15877  lspdisjb  15879  islbs2  15907  islbs3  15908  issubassa  16064  issubassa2  16084  gsumbagdiag  16122  subrgasclcl  16240  prmirredlem  16446  en2top  16723  elcls  16810  neindisj2  16860  maxlp  16878  iscncl  16998  cncnp  17009  isreg2  17105  dis2ndc  17186  1stccnp  17188  islly2  17210  dislly  17223  kgencmp2  17241  pt1hmeo  17497  xkocnv  17505  t0kq  17509  uffixfr  17618  flimcf  17677  cnpflf2  17695  fclscf  17720  tngngp2  18168  tngngp  18170  nmoleub  18240  metdseq0  18358  cnheibor  18453  pcophtb  18527  nmoleub2lem  18595  lmmbr  18684  iscfil3  18699  cmetss  18740  cldcss  18805  mbfeqalem  18997  mbfposb  19008  itg2const2  19096  itgss3  19169  plyco0  19574  dgrlt  19647  ulm2  19764  coseq00topi  19870  coseq0negpitopi  19871  sineq0  19889  atans2  20227  xrlimcnp  20263  dchrelbas2  20476  dchrn0  20489  2sqb  20617  grpoinvid1  20897  grpoinvid2  20898  ismndo1  21011  leopmul  22714  hst1h  22807  fzsplit3  23031  f1o3d  23037  sconpi1  23770  brofs2  24700  brifs2  24701  broutsideof2  24745  repfuntw  25160  imonclem  25813  pdiveql  26168  isdrngo2  26589  mrefg2  26782  mzpmfp  26825  lzenom  26849  elpell14qr2  26947  elpell1qr2  26957  pellfund14b  26984  congabseq  27061  acongeq  27070  jm2.23  27089  jm2.20nn  27090  jm2.25lem1  27091  wepwsolem  27138  islssfg2  27169  lnmlmic  27186  dfacbasgrp  27273  islindf3  27296  lindsmm  27298  lsslindf  27300  lsslinds  27301  rfcnpre3  27704  rfcnpre4  27705  lshpnelb  29174  lshpnel2N  29175  lsatspn0  29190  lsatelbN  29196  lsat0cv  29223  lcvexch  29229  lcv1  29231  lkrshp3  29296  lkrpssN  29353  lkrss2N  29359  cvlsupr2  29533  atcvrlln  29709  llncvrlpln  29747  2llnmj  29749  lplncvrlvol  29805  2lplnmj  29811  polcon2bN  30109  pcl0bN  30112  lhpmcvr3  30214  lhpmatb  30220  ltrncoidN  30317  ltrneq3  30397  ltrniotavalbN  30773  cdlemg1cN  30776  diclspsn  31384  dihopelvalcpre  31438  dihord4  31448  dihord  31454  dihmeetlem4preN  31496  dih1dimatlem0  31518  dochsscl  31558  dochoccl  31559  dochord  31560  dochsat  31573  dochshpncl  31574  dochsatshpb  31642  dochshpsat  31644  mapdval4N  31822  mapdsn  31831  hdmap14lem12  32072  hdmapip0  32108  hlhillcs  32151
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 177  df-an 360
  Copyright terms: Public domain W3C validator