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

Theorem biimpar 471
Description: Inference from a logical equivalence. (Contributed by NM, 3-May-1994.)
Hypothesis
Ref Expression
biimpa.1  |-  ( ph  ->  ( ps  <->  ch )
)
Assertion
Ref Expression
biimpar  |-  ( (
ph  /\  ch )  ->  ps )

Proof of Theorem biimpar
StepHypRef Expression
1 biimpa.1 . . 3  |-  ( ph  ->  ( ps  <->  ch )
)
21biimprd 214 . 2  |-  ( ph  ->  ( ch  ->  ps ) )
32imp 418 1  |-  ( (
ph  /\  ch )  ->  ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 176    /\ wa 358
This theorem is referenced by:  exbiri  605  bitr  689  oplem1  930  eqtr  2383  opabss  4182  euotd  4370  xpsspw  4900  somin1  5182  funfni  5449  fnco  5457  fnssres  5462  fn0  5468  fnimadisj  5469  fnimaeq0  5470  foco  5567  foimacnv  5596  fvelimab  5685  dffv2  5699  fvopab3ig  5706  dff3  5784  dffo4  5787  fnexALT  5862  f1eqcocnv  5928  isomin  5957  f1ocnv2d  6195  xp1st  6276  xp2nd  6277  iinon  6499  tfrlem1  6533  tfr3  6557  oawordri  6690  oaass  6701  omeulem1  6722  oeoa  6737  oeoe  6739  oeeulem  6741  ecelqsg  6856  elqsn0  6870  pwdom  7156  marypha1lem  7333  wofib  7407  cantnff  7522  cantnfp1  7530  cantnf  7542  cnfcomlem  7549  r1sscl  7604  rankval3b  7645  infxpidm2  7791  numdom  7812  onssnum  7814  acni  7819  acni2  7820  dfac5  7902  cdalepw  7969  infunsdom1  7986  infunsdom  7987  cofsmo  8042  cfsmolem  8043  fin1ai  8066  fin2i  8068  isf34lem1  8145  fin67  8168  itunisuc  8192  axdc3lem4  8226  zornn0g  8279  ttukeylem6  8288  brdom3  8300  tsken  8523  tskcard  8550  r1tskina  8551  intgru  8583  prlem934  8804  ltexprlem7  8813  uzindOLD  10257  xrmaxeq  10660  xrmineq  10661  xmulneg1  10741  ixxun  10825  fzm1  11017  elfznelfzo  11079  btwnzge0  11117  ioopnfsup  11132  icopnfsup  11133  faclbnd4lem4  11474  hasheni  11519  hashgt0  11549  hashge1  11550  hashprb  11555  lennncl  11623  ccatlid  11635  ccatass  11637  swrdid  11659  ccatswrd  11660  swrdccat2  11662  revccat  11685  cnpart  11932  resqreu  11945  recval  12013  abs1m  12026  abslem2  12030  fzomaxdiflem  12033  sqreulem  12050  sqreu  12051  limsupgre  12162  rlimdiv  12326  fsumparts  12472  climcnds  12518  expcnv  12530  ndvdssub  12814  sadcaddlem  12856  rplpwr  12943  dvdssqlem  12946  algcvgblem  12955  eucalgcvga  12964  coprimeprodsq  13070  pythagtriplem11  13086  pythagtriplem13  13088  pcadd2  13146  4sqlem11  13210  vdwlem6  13241  vdwlem8  13243  vdwlem10  13245  ramval  13263  ramcl2  13271  ramlb  13274  ram0  13277  mreintcl  13707  mrcval  13722  mrccl  13723  mrcuni  13733  mrcun  13734  acsfiel  13766  rescabs  13920  funcres  13980  setcmon  14129  setcepi  14130  yonffthlem  14266  pleval2i  14308  pospo  14317  poslubdg  14462  acsdrsel  14480  acsdrscl  14483  acsficl  14484  psss  14533  grpidd  14605  ismndd  14606  gsumccat  14674  gsumwmhm  14677  subgmulg  14845  resghm  14909  conjnsg  14928  lsmelvalix  15162  pj1ghm  15222  efgredlemc  15264  frgp0  15279  divsabl  15367  cycsubgcyg  15397  gsumval3  15401  gsumcllem  15403  ablfac1c  15516  pgpfac1lem5  15524  isrngd  15585  lspsneq0b  15980  lmodindp1  15981  lmhmf1o  16013  lmhmpreima  16015  reslmhm  16019  lspsncmp  16079  lspsneq  16085  znf1o  16722  uniopn  16860  ntrval  16990  clsval  16991  neival  17056  lpval  17088  restdis  17126  lmbrf  17207  cnpnei  17210  1stcrest  17396  hauspwdom  17444  txcnpi  17519  ptrescn  17550  xkococnlem  17570  qtopeu  17624  kqreglem1  17649  ptuncnv  17715  filss  17761  fsubbas  17775  fbasrn  17792  cfinfil  17801  ufinffr  17837  elfm3  17858  rnelfmlem  17860  rnelfm  17861  flimclslem  17892  flfval  17898  isfcf  17942  met1stc  18280  nmoix  18451  nmoeq0  18458  idnghm  18465  blcvx  18517  xrsxmet  18528  iccntr  18540  icccmp  18544  iihalf1  18644  iihalf2  18646  xrhmeo  18659  cnheibor  18668  ipcau2  18879  lmmbrf  18903  iscauf  18921  cmetcaulem  18929  bcthlem4  18964  minveclem4  19011  evthicc2  19035  cniccbdd  19036  ovollb2  19063  ovolunlem1a  19070  ovolunlem1  19071  voliun  19126  icombl  19136  ioombl  19137  iccvolcl  19139  mbfss  19216  mbfposb  19223  itg2const2  19311  itg2splitlem  19318  itg2gt0  19330  iblss2  19375  itgioo  19385  dvaddf  19506  dvmulf  19507  dvcobr  19510  dvcof  19512  rolle  19552  dvlip  19555  c1lip1  19559  dvivthlem1  19570  lhop1lem  19575  dvfsumlem1  19588  ftc1lem4  19601  ftc1lem5  19602  mpfind  19643  ply1divmo  19736  coe1termlem  19854  plydiveu  19893  taylplem1  19957  pserulm  20016  abelth  20035  abscxp2  20262  abscxpbnd  20315  ang180lem2  20330  ang180lem3  20331  isosctrlem1  20340  angpieqvd  20350  atandmtan  20438  birthdaylem3  20470  wilthlem2  20530  isppw  20575  isppw2  20576  dvdsflsumcom  20651  chteq0  20671  perfectlem2  20692  dchrval  20696  dchrinvcl  20715  dchrptlem1  20726  bposlem3  20748  lgsmod  20783  lgsdilem  20784  lgsdir2lem2  20786  lgsdir2  20790  lgsne0  20795  lgseisenlem1  20811  2sqlem4  20829  chpo1ubb  20853  dchrisumn0  20893  pntrsumbnd2  20939  ostthlem1  20999  ostth3  21010  uvtxnbgravtx  21174  gxcom  21368  resgrprn  21379  ghablo  21468  nvss  21583  sspn  21746  nmoub3i  21785  nmblolbii  21811  blocnilem  21816  minvecolem4  21893  htthlem  21931  norm1  22262  norm1exi  22263  pjeq  22412  axpjpj  22433  normcan  22589  pjoi0  22730  nmopub2tALT  22923  nmfnleub2  22940  eighmorth  22978  nmbdoplbi  23038  nmcoplbi  23042  nmophmi  23045  nmbdfnlbi  23063  nmcfnlbi  23066  riesz3i  23076  cnlnadjlem7  23087  branmfn  23119  nmopleid  23153  hstle  23244  superpos  23368  cvexchlem  23382  elabreximd  23507  f1o3d  23565  funcnvmptOLD  23605  funcnvmpt  23606  xrofsup  23647  eliccelico  23662  elicoelioo  23663  difioo  23667  neiptopreu  23766  unitdivcld  23775  cnextfvval  23822  cnextf  23823  cnextcn  23824  trust  23853  restutop  23861  ustuqtop2  23866  metustexhalf  23920  cfilucfil  23923  metutop  23931  cmetcusp  23934  elzrhunit  23956  qqhf  23963  indf1ofs  24009  gsumesum  24037  esumfsup  24046  esumcvg  24062  issgon  24092  sigainb  24105  insiga  24106  isrnmeas  24140  measvunilem  24150  volmeas  24171  imambfm  24196  probun  24246  dstfrvunirn  24301  derangen  24427  subfacp1lem2b  24436  subfacp1lem4  24438  subfacp1lem5  24439  derangfmla  24445  ptpcon  24488  ntrivcvg  24794  wfr3g  25081  wfrlem3  25084  wfrlem4  25085  frr3g  25106  frrlem3  25109  nocvxmin  25171  nobndlem6  25177  nobndup  25180  nobnddown  25181  brcgr  25355  colinearalglem4  25364  colinearalg  25365  axlowdimlem14  25410  axcontlem4  25422  colinearex  25510  btwnconn1lem11  25547  btwnconn1lem12  25548  supaddc  25750  voliunnfl  25758  itg2addnclem  25760  itg2addnc  25762  itg2gt0cn  25763  ftc1cnnclem  25781  gtinf  25826  nn0prpwlem  25830  lfinpfin  25895  cover2  25950  indexdom  26005  sdclem1  26045  fdc  26047  equivbnd2  26107  heiborlem8  26133  heibor  26136  isdrngo2  26180  iscringd  26215  smprngopr  26268  prnc  26283  nacsfix  26378  3rexfrabdioph  26469  4rexfrabdioph  26470  6rexfrabdioph  26471  7rexfrabdioph  26472  eldioph4b  26485  pellexlem2  26506  pellexlem5  26509  expmordi  26623  jm2.26lem3  26685  pwssplit3  26781  dsmmlss  26801  frlmlbs  26840  frlmup1  26841  numinfctb  26859  f1otrspeq  26981  pmtrval  26985  pmtrrn  26990  pmtrfinv  26993  psgnunilem1  27007  psgnunilem5  27008  psgnunilem4  27011  psgneldm2i  27019  mat1  27073  dvconstbi  27142  ioovolcl  27333  stoweidlem27  27367  stoweidlem28  27368  stoweidlem34  27374  onetansqsecsq  27921  cotsqcscsq  27922  elpwgded  28065  elpwgdedVD  28445  sspwimpcf  28448  sspwimpcfVD  28449  sspwimpALT2  28457  a9e2ndeqALT  28460  bnj529  28522  bnj548  28681  bnj570  28689  bnj852  28705  bnj929  28720  bnj1097  28763  bnj1118  28766  bnj1145  28775  islfld  29311  lkrshpor  29356  lfl1dim  29370  lfl1dim2N  29371  cmtcomlemN  29497  2lplnmN  29807  pmapjat1  30101  trlnid  30427  tendoex  31223  dia1dimid  31312  dibval2  31393  dihmeetlem2N  31548  dochlkr  31634  mapdcv  31909  hdmaplkr  32165  hdmapip0  32167  hlhillcs  32210
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