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  2300  opabss  4080  euotd  4267  xpsspw  4797  somin1  5079  funfni  5344  fnco  5352  fnssres  5357  fn0  5363  fnimadisj  5364  fnimaeq0  5365  foco  5461  foimacnv  5490  fvelimab  5578  dffv2  5592  fvopab3ig  5599  dff3  5673  dffo4  5676  fnexALT  5742  f1eqcocnv  5805  isomin  5834  f1ocnv2d  6068  xp1st  6149  xp2nd  6150  iinon  6357  tfrlem1  6391  tfr3  6415  oawordri  6548  oaass  6559  omeulem1  6580  oeoa  6595  oeoe  6597  oeeulem  6599  ecelqsg  6714  elqsn0  6728  pwdom  7013  marypha1lem  7186  wofib  7260  cantnff  7375  cantnfp1  7383  cantnf  7395  cnfcomlem  7402  r1sscl  7457  rankval3b  7498  infxpidm2  7644  numdom  7665  onssnum  7667  acni  7672  acni2  7673  dfac5  7755  cdalepw  7822  infunsdom1  7839  infunsdom  7840  cofsmo  7895  cfsmolem  7896  fin1ai  7919  fin2i  7921  isf34lem1  7998  fin67  8021  itunisuc  8045  axdc3lem4  8079  zornn0g  8132  ttukeylem6  8141  brdom3  8153  tsken  8376  tskcard  8403  r1tskina  8404  intgru  8436  prlem934  8657  ltexprlem7  8666  uzindOLD  10106  xrmaxeq  10508  xrmineq  10509  xmulneg1  10589  ixxun  10672  fzm1  10862  btwnzge0  10953  ioopnfsup  10968  icopnfsup  10969  faclbnd4lem4  11309  hasheni  11347  lennncl  11422  ccatlid  11434  ccatass  11436  swrdid  11458  ccatswrd  11459  swrdccat2  11461  revccat  11484  cnpart  11725  resqreu  11738  recval  11806  abs1m  11819  abslem2  11823  fzomaxdiflem  11826  sqreulem  11843  sqreu  11844  limsupgre  11955  rlimdiv  12119  fsumparts  12264  climcnds  12310  expcnv  12322  ndvdssub  12606  sadcaddlem  12648  rplpwr  12735  dvdssqlem  12738  algcvgblem  12747  eucalgcvga  12756  coprimeprodsq  12862  pythagtriplem11  12878  pythagtriplem13  12880  pcadd2  12938  4sqlem11  13002  vdwlem6  13033  vdwlem8  13035  vdwlem10  13037  ramval  13055  ramcl2  13063  ramlb  13066  ram0  13069  mreintcl  13497  mrcval  13512  mrccl  13513  mrcuni  13523  mrcun  13524  acsfiel  13556  rescabs  13710  funcres  13770  setcmon  13919  setcepi  13920  yonffthlem  14056  pleval2i  14098  pospo  14107  poslubdg  14252  acsdrsel  14270  acsdrscl  14273  acsficl  14274  psss  14323  grpidd  14395  ismndd  14396  gsumccat  14464  gsumwmhm  14467  subgmulg  14635  resghm  14699  conjnsg  14718  lsmelvalix  14952  pj1ghm  15012  efgredlemc  15054  frgp0  15069  divsabl  15157  cycsubgcyg  15187  gsumval3  15191  gsumcllem  15193  ablfac1c  15306  pgpfac1lem5  15314  isrngd  15375  lspsneq0b  15770  lmodindp1  15771  lmhmf1o  15803  lmhmpreima  15805  reslmhm  15809  lspsncmp  15869  lspsneq  15875  znf1o  16505  uniopn  16643  ntrval  16773  clsval  16774  neival  16839  lpval  16871  restdis  16909  lmbrf  16990  cnpnei  16993  1stcrest  17179  hauspwdom  17227  txcnpi  17302  ptrescn  17333  xkococnlem  17353  qtopeu  17407  kqreglem1  17432  ptuncnv  17498  filss  17548  fsubbas  17562  fbasrn  17579  cfinfil  17588  ufinffr  17624  elfm3  17645  rnelfmlem  17647  rnelfm  17648  flimclslem  17679  flfval  17685  isfcf  17729  met1stc  18067  nmoix  18238  nmoeq0  18245  idnghm  18252  blcvx  18304  xrsxmet  18315  iccntr  18326  icccmp  18330  iihalf1  18429  iihalf2  18431  xrhmeo  18444  cnheibor  18453  ipcau2  18664  lmmbrf  18688  iscauf  18706  cmetcaulem  18714  bcthlem4  18749  minveclem4  18796  evthicc2  18820  cniccbdd  18821  ovollb2  18848  ovolunlem1a  18855  ovolunlem1  18856  voliun  18911  icombl  18921  ioombl  18922  iccvolcl  18924  mbfss  19001  mbfposb  19008  itg2const2  19096  itg2splitlem  19103  itg2gt0  19115  iblss2  19160  itgioo  19170  dvaddf  19291  dvmulf  19292  dvcobr  19295  dvcof  19297  rolle  19337  dvlip  19340  c1lip1  19344  dvivthlem1  19355  lhop1lem  19360  dvfsumlem1  19373  ftc1lem4  19386  ftc1lem5  19387  mpfind  19428  ply1divmo  19521  coe1termlem  19639  plydiveu  19678  taylplem1  19742  pserulm  19798  abelth  19817  abscxp2  20040  abscxpbnd  20093  ang180lem2  20108  ang180lem3  20109  isosctrlem1  20118  angpieqvd  20128  atandmtan  20216  birthdaylem3  20248  wilthlem2  20307  isppw  20352  isppw2  20353  dvdsflsumcom  20428  chteq0  20448  perfectlem2  20469  dchrval  20473  dchrinvcl  20492  dchrptlem1  20503  bposlem3  20525  lgsmod  20560  lgsdilem  20561  lgsdir2lem2  20563  lgsdir2  20567  lgsne0  20572  lgseisenlem1  20588  2sqlem4  20606  chpo1ubb  20630  dchrisumn0  20670  pntrsumbnd2  20716  ostthlem1  20776  ostth3  20787  gxcom  20936  resgrprn  20947  ghablo  21036  nvss  21149  sspn  21312  nmoub3i  21351  nmblolbii  21377  blocnilem  21382  minvecolem4  21459  htthlem  21497  norm1  21828  norm1exi  21829  pjeq  21978  axpjpj  21999  normcan  22155  pjoi0  22296  nmopub2tALT  22489  nmfnleub2  22506  eighmorth  22544  nmbdoplbi  22604  nmcoplbi  22608  nmophmi  22611  nmbdfnlbi  22629  nmcfnlbi  22632  riesz3i  22642  cnlnadjlem7  22653  branmfn  22685  nmopleid  22719  hstle  22810  superpos  22934  cvexchlem  22948  f1o3d  23037  elabreximd  23039  funcnvmptOLD  23234  funcnvmpt  23235  xrofsup  23255  eliccelico  23270  elicoelioo  23271  difioo  23275  unitdivcld  23285  hashgt0  23387  hashge1  23388  esumcvg  23454  issgon  23484  sigainb  23497  insiga  23498  isrnmeas  23531  measvunilem  23540  imambfm  23567  indf1ofs  23609  probun  23622  dstfrvunirn  23675  derangen  23703  subfacp1lem2b  23712  subfacp1lem4  23714  subfacp1lem5  23715  derangfmla  23721  ptpcon  23764  wfr3g  24255  wfrlem3  24258  wfrlem4  24259  frr3g  24280  frrlem3  24283  nocvxmin  24345  nobndlem6  24351  nobndup  24354  nobnddown  24355  brcgr  24528  colinearalglem4  24537  colinearalg  24538  axlowdimlem14  24583  axcontlem4  24595  colinearex  24683  btwnconn1lem11  24720  btwnconn1lem12  24721  cbicp  25166  supdef  25262  mapudiscn  25528  cmpmorp  25779  dualcat2  25784  vtare  25885  gtinf  26234  nn0prpwlem  26238  lfinpfin  26303  cover2  26358  indexdom  26413  sdclem1  26453  fdc  26455  equivbnd2  26516  heiborlem8  26542  heibor  26545  isdrngo2  26589  iscringd  26624  smprngopr  26677  prnc  26692  nacsfix  26787  3rexfrabdioph  26878  4rexfrabdioph  26879  6rexfrabdioph  26880  7rexfrabdioph  26881  eldioph4b  26894  pellexlem2  26915  pellexlem5  26918  expmordi  27032  jm2.26lem3  27094  pwssplit3  27190  dsmmlss  27210  frlmlbs  27249  frlmup1  27250  numinfctb  27268  f1otrspeq  27390  pmtrval  27394  pmtrrn  27399  pmtrfinv  27402  psgnunilem1  27416  psgnunilem5  27417  psgnunilem4  27420  psgneldm2i  27428  mat1  27482  dvconstbi  27551  ioovolcl  27742  stoweidlem27  27776  stoweidlem28  27777  stoweidlem34  27783  uvtxnbgravtx  28167  onetansqsecsq  28231  cotsqcscsq  28232  elpwgded  28330  elpwgdedVD  28693  sspwimpcf  28696  sspwimpcfVD  28697  sspwimpALT2  28705  a9e2ndeqALT  28708  bnj529  28770  bnj548  28929  bnj570  28937  bnj852  28953  bnj929  28968  bnj1097  29011  bnj1118  29014  bnj1145  29023  islfld  29252  lkrshpor  29297  lfl1dim  29311  lfl1dim2N  29312  cmtcomlemN  29438  2lplnmN  29748  pmapjat1  30042  trlnid  30368  tendoex  31164  dia1dimid  31253  dibval2  31334  dihmeetlem2N  31489  dochlkr  31575  mapdcv  31850  hdmaplkr  32106  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