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  2295  frsn  4776  funfvbrb  5654  iinpreima  5671  f1ocnv2d  6084  1stconst  6223  2ndconst  6224  cnvf1o  6233  tfrlem15  6424  oeeui  6616  ersymb  6690  swoer  6704  erth  6720  boxriin  6874  boxcutc  6875  domunsncan  6978  pw2f1olem  6982  enen1  7017  enen2  7018  domen1  7019  domen2  7020  sdomen1  7021  sdomen2  7022  xpmapenlem  7044  ordiso2  7246  wdomen1  7306  wdomen2  7307  fin23lem26  7967  fpwwe2lem8  8275  r1wunlim  8375  ixxun  10688  xov1plusxeqvd  10796  fzsplit2  10831  elfz2nn0  10837  fseq1p1m1  10873  modsubdir  11024  zesq  11240  hashprg  11384  hashbclem  11406  rereb  11621  rlimclim  12036  iserex  12146  caucvgb  12168  fsumrev  12257  fsumshft  12258  climcnds  12326  dvdsadd2b  12587  bitsfzo  12642  dvdsmulgcd  12749  qden1elz  12844  mrcidb  13533  mrieqvlemd  13547  isacs2  13571  ssclem  13712  issubc3  13739  ffthiso  13819  fuciso  13865  setcmon  13935  setcepi  13936  setcinv  13938  catciso  13955  acsfiindd  14296  issubmnd  14417  subsubm  14450  resmhm2b  14454  grpinvid1  14546  grpinvid2  14547  subsubg  14656  ssnmz  14675  ghmf1  14727  ghmf1o  14728  conjnmzb  14733  subggim  14746  gicsubgen  14758  gass  14771  odf1  14891  gex1  14918  fislw  14952  sylow3lem2  14955  sylow3lem6  14959  lsmdisj2a  15012  lsmdisj2b  15013  efgred2  15078  dmdprdsplit  15298  0unit  15478  irrednegb  15509  isdrng2  15538  subrgunit  15579  issubdrg  15586  subsubrg  15587  islss3  15732  islss4  15735  lspsnel6  15767  lspsneq0b  15786  islmhm2  15811  lmhmf1o  15819  reslmhm2b  15827  lssvs0or  15879  lvecinv  15882  lspsnel4  15893  lspdisjb  15895  islbs2  15923  islbs3  15924  issubassa  16080  issubassa2  16100  gsumbagdiag  16138  subrgasclcl  16256  prmirredlem  16462  en2top  16739  elcls  16826  neindisj2  16876  maxlp  16894  iscncl  17014  cncnp  17025  isreg2  17121  dis2ndc  17202  1stccnp  17204  islly2  17226  dislly  17239  kgencmp2  17257  pt1hmeo  17513  xkocnv  17521  t0kq  17525  uffixfr  17634  flimcf  17693  cnpflf2  17711  fclscf  17736  tngngp2  18184  tngngp  18186  nmoleub  18256  metdseq0  18374  cnheibor  18469  pcophtb  18543  nmoleub2lem  18611  lmmbr  18700  iscfil3  18715  cmetss  18756  cldcss  18821  mbfeqalem  19013  mbfposb  19024  itg2const2  19112  itgss3  19185  plyco0  19590  dgrlt  19663  ulm2  19780  coseq00topi  19886  coseq0negpitopi  19887  sineq0  19905  atans2  20243  xrlimcnp  20279  dchrelbas2  20492  dchrn0  20505  2sqb  20633  grpoinvid1  20913  grpoinvid2  20914  ismndo1  21027  leopmul  22730  hst1h  22823  fzsplit3  23047  f1o3d  23053  sconpi1  23785  brofs2  24772  brifs2  24773  broutsideof2  24817  ltflcei  24998  lxflflp1  25000  repfuntw  25263  imonclem  25916  pdiveql  26271  isdrngo2  26692  mrefg2  26885  mzpmfp  26928  lzenom  26952  elpell14qr2  27050  elpell1qr2  27060  pellfund14b  27087  congabseq  27164  acongeq  27173  jm2.23  27192  jm2.20nn  27193  jm2.25lem1  27194  wepwsolem  27241  islssfg2  27272  lnmlmic  27289  dfacbasgrp  27376  islindf3  27399  lindsmm  27401  lsslindf  27403  lsslinds  27404  rfcnpre3  27807  rfcnpre4  27808  nb3graprlem1  28287  lshpnelb  29796  lshpnel2N  29797  lsatspn0  29812  lsatelbN  29818  lsat0cv  29845  lcvexch  29851  lcv1  29853  lkrshp3  29918  lkrpssN  29975  lkrss2N  29981  cvlsupr2  30155  atcvrlln  30331  llncvrlpln  30369  2llnmj  30371  lplncvrlvol  30427  2lplnmj  30433  polcon2bN  30731  pcl0bN  30734  lhpmcvr3  30836  lhpmatb  30842  ltrncoidN  30939  ltrneq3  31019  ltrniotavalbN  31395  cdlemg1cN  31398  diclspsn  32006  dihopelvalcpre  32060  dihord4  32070  dihord  32076  dihmeetlem4preN  32118  dih1dimatlem0  32140  dochsscl  32180  dochoccl  32181  dochord  32182  dochsat  32195  dochshpncl  32196  dochsatshpb  32264  dochshpsat  32266  mapdval4N  32444  mapdsn  32453  hdmap14lem12  32694  hdmapip0  32730  hlhillcs  32773
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