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

Theorem biimpar 472
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 215 . 2  |-  ( ph  ->  ( ch  ->  ps ) )
32imp 419 1  |-  ( (
ph  /\  ch )  ->  ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 177    /\ wa 359
This theorem is referenced by:  exbiri  606  bitr  690  oplem1  931  eqtr  2421  opabss  4229  euotd  4417  xpsspw  4945  brcogw  5000  somin1  5229  funfni  5504  fnco  5512  fnssres  5517  fn0  5523  fnimadisj  5524  fnimaeq0  5525  foco  5622  foimacnv  5651  fvelimab  5741  dffv2  5755  fvopab3ig  5762  dff3  5841  dffo4  5844  fnexALT  5921  f1eqcocnv  5987  isomin  6016  f1ocnv2d  6254  xp1st  6335  xp2nd  6336  iinon  6561  tfrlem1  6595  tfr3  6619  oawordri  6752  oaass  6763  omeulem1  6784  oeoa  6799  oeoe  6801  oeeulem  6803  ecelqsg  6918  elqsn0  6932  pwdom  7218  marypha1lem  7396  wofib  7470  cantnff  7585  cantnfp1  7593  cantnf  7605  cnfcomlem  7612  r1sscl  7667  rankval3b  7708  infxpidm2  7854  numdom  7875  onssnum  7877  acni  7882  acni2  7883  dfac5  7965  cdalepw  8032  infunsdom1  8049  infunsdom  8050  cofsmo  8105  cfsmolem  8106  fin1ai  8129  fin2i  8131  isf34lem1  8208  fin67  8231  itunisuc  8255  axdc3lem4  8289  zornn0g  8341  ttukeylem6  8350  brdom3  8362  tsken  8585  tskcard  8612  r1tskina  8613  intgru  8645  prlem934  8866  ltexprlem7  8875  uzindOLD  10320  xrmaxeq  10723  xrmineq  10724  xmulneg1  10804  ixxun  10888  fzm1  11082  elfznelfzo  11147  btwnzge0  11185  ioopnfsup  11200  icopnfsup  11201  faclbnd4lem4  11542  hasheni  11587  hashgt0  11617  hashge1  11618  hashprb  11623  lennncl  11691  ccatlid  11703  ccatass  11705  swrdid  11727  ccatswrd  11728  swrdccat2  11730  revccat  11753  cnpart  12000  resqreu  12013  recval  12081  abs1m  12094  abslem2  12098  fzomaxdiflem  12101  sqreulem  12118  sqreu  12119  limsupgre  12230  rlimdiv  12394  fsumparts  12540  climcnds  12586  expcnv  12598  ndvdssub  12882  sadcaddlem  12924  rplpwr  13011  dvdssqlem  13014  algcvgblem  13023  eucalgcvga  13032  coprimeprodsq  13138  pythagtriplem11  13154  pythagtriplem13  13156  pcadd2  13214  4sqlem11  13278  vdwlem6  13309  vdwlem8  13311  vdwlem10  13313  ramval  13331  ramcl2  13339  ramlb  13342  ram0  13345  mreintcl  13775  mrcval  13790  mrccl  13791  mrcuni  13801  mrcun  13802  acsfiel  13834  rescabs  13988  funcres  14048  setcmon  14197  setcepi  14198  yonffthlem  14334  pleval2i  14376  pospo  14385  poslubdg  14530  acsdrsel  14548  acsdrscl  14551  acsficl  14552  psss  14601  grpidd  14673  ismndd  14674  gsumccat  14742  gsumwmhm  14745  subgmulg  14913  resghm  14977  conjnsg  14996  lsmelvalix  15230  pj1ghm  15290  efgredlemc  15332  frgp0  15347  divsabl  15435  cycsubgcyg  15465  gsumval3  15469  gsumcllem  15471  ablfac1c  15584  pgpfac1lem5  15592  isrngd  15653  lspsneq0b  16044  lmodindp1  16045  lmhmf1o  16077  lmhmpreima  16079  reslmhm  16083  lspsncmp  16143  lspsneq  16149  znf1o  16787  uniopn  16925  ntrval  17055  clsval  17056  neival  17121  neiptopreu  17152  lpval  17158  restdis  17196  lmbrf  17278  cnpnei  17282  1stcrest  17469  hauspwdom  17517  txcnpi  17593  ptrescn  17624  xkococnlem  17644  qtopeu  17701  kqreglem1  17726  ptuncnv  17792  filss  17838  fsubbas  17852  fbasrn  17869  cfinfil  17878  ufinffr  17914  elfm3  17935  rnelfmlem  17937  rnelfm  17938  flimclslem  17969  flfval  17975  isfcf  18019  cnextfvval  18049  cnextf  18050  cnextcn  18051  ustelimasn  18205  trust  18212  restutop  18220  ustuqtop2  18225  utop2nei  18233  ucncn  18268  trcfilu  18277  cnextucn  18286  met1stc  18504  metustexhalfOLD  18546  metustexhalf  18547  cfilucfilOLD  18552  cfilucfil  18553  metutopOLD  18565  psmetutop  18566  nmoix  18716  nmoeq0  18723  idnghm  18730  blcvx  18782  xrsxmet  18793  iccntr  18805  icccmp  18809  iihalf1  18909  iihalf2  18911  xrhmeo  18924  cnheibor  18933  ipcau2  19144  lmmbrf  19168  iscauf  19186  cmetcaulem  19194  bcthlem4  19233  cmetcuspOLD  19260  cmetcusp  19261  minveclem4  19286  evthicc2  19310  cniccbdd  19311  ovollb2  19338  ovolunlem1a  19345  ovolunlem1  19346  voliun  19401  icombl  19411  ioombl  19412  iccvolcl  19414  mbfss  19491  mbfposb  19498  itg2const2  19586  itg2splitlem  19593  itg2gt0  19605  iblss2  19650  itgioo  19660  dvaddf  19781  dvmulf  19782  dvcobr  19785  dvcof  19787  rolle  19827  dvlip  19830  c1lip1  19834  dvivthlem1  19845  lhop1lem  19850  dvfsumlem1  19863  ftc1lem4  19876  ftc1lem5  19877  mpfind  19918  ply1divmo  20011  coe1termlem  20129  plydiveu  20168  taylplem1  20232  pserulm  20291  abelth  20310  abscxp2  20537  abscxpbnd  20590  ang180lem2  20605  ang180lem3  20606  isosctrlem1  20615  angpieqvd  20625  atandmtan  20713  birthdaylem3  20745  wilthlem2  20805  isppw  20850  isppw2  20851  dvdsflsumcom  20926  chteq0  20946  perfectlem2  20967  dchrval  20971  dchrinvcl  20990  dchrptlem1  21001  bposlem3  21023  lgsmod  21058  lgsdilem  21059  lgsdir2lem2  21061  lgsdir2  21065  lgsne0  21070  lgseisenlem1  21086  2sqlem4  21104  chpo1ubb  21128  dchrisumn0  21168  pntrsumbnd2  21214  ostthlem1  21274  ostth3  21285  uvtxnbgravtx  21457  gxcom  21810  resgrprn  21821  ghablo  21910  nvss  22025  sspn  22188  nmoub3i  22227  nmblolbii  22253  blocnilem  22258  minvecolem4  22335  htthlem  22373  norm1  22704  norm1exi  22705  pjeq  22854  axpjpj  22875  normcan  23031  pjoi0  23172  nmopub2tALT  23365  nmfnleub2  23382  eighmorth  23420  nmbdoplbi  23480  nmcoplbi  23484  nmophmi  23487  nmbdfnlbi  23505  nmcfnlbi  23508  riesz3i  23518  cnlnadjlem7  23529  branmfn  23561  nmopleid  23595  hstle  23686  superpos  23810  cvexchlem  23824  elabreximd  23944  f1o3d  23994  funcnvmptOLD  24035  funcnvmpt  24036  xrofsup  24079  eliccelico  24093  elicoelioo  24094  iocinif  24097  difioo  24098  eliccioo  24130  subofld  24198  unitdivcld  24252  tpr2rico  24263  lmxrge0  24290  elzrhunit  24316  qqhf  24323  indf1ofs  24376  gsumesum  24404  esumfsup  24413  esumcvg  24429  issgon  24459  sigainb  24472  insiga  24473  isrnmeas  24507  measvunilem  24519  volmeas  24540  imambfm  24565  probun  24630  dstfrvunirn  24685  derangen  24811  subfacp1lem2b  24820  subfacp1lem4  24822  subfacp1lem5  24823  derangfmla  24829  ptpcon  24873  ntrivcvg  25178  wfr3g  25469  wfrlem3  25472  wfrlem4  25473  frr3g  25494  frrlem3  25497  nocvxmin  25559  nobndlem6  25565  nobndup  25568  nobnddown  25569  brcgr  25743  colinearalglem4  25752  colinearalg  25753  axlowdimlem14  25798  axcontlem4  25810  colinearex  25898  btwnconn1lem11  25935  btwnconn1lem12  25936  supaddc  26137  mblfinlem  26143  voliunnfl  26149  mbfresfi  26152  itg2addnclem  26155  itg2addnclem3  26157  itg2gt0cn  26159  ftc1cnnclem  26177  gtinf  26212  nn0prpwlem  26215  lfinpfin  26273  cover2  26305  indexdom  26326  sdclem1  26337  fdc  26339  equivbnd2  26391  heiborlem8  26417  heibor  26420  isdrngo2  26464  iscringd  26499  smprngopr  26552  prnc  26567  nacsfix  26656  3rexfrabdioph  26747  4rexfrabdioph  26748  6rexfrabdioph  26749  7rexfrabdioph  26750  eldioph4b  26762  pellexlem2  26783  pellexlem5  26786  expmordi  26900  jm2.26lem3  26962  pwssplit3  27058  dsmmlss  27078  frlmlbs  27117  frlmup1  27118  numinfctb  27136  f1otrspeq  27258  pmtrval  27262  pmtrrn  27267  pmtrfinv  27270  psgnunilem1  27284  psgnunilem5  27285  psgnunilem4  27288  psgneldm2i  27296  mat1  27350  dvconstbi  27419  ioovolcl  27609  stoweidlem27  27643  stoweidlem28  27644  swrdltnd  28000  swrdnd  28001  frghash2spot  28166  onetansqsecsq  28218  cotsqcscsq  28219  elpwgded  28362  elpwgdedVD  28738  sspwimpcf  28741  sspwimpcfVD  28742  sspwimpALT2  28750  a9e2ndeqALT  28753  bnj529  28815  bnj548  28974  bnj570  28982  bnj852  28998  bnj929  29013  bnj1097  29056  bnj1118  29059  bnj1145  29068  islfld  29545  lkrshpor  29590  lfl1dim  29604  lfl1dim2N  29605  cmtcomlemN  29731  2lplnmN  30041  pmapjat1  30335  trlnid  30661  tendoex  31457  dia1dimid  31546  dibval2  31627  dihmeetlem2N  31782  dochlkr  31868  mapdcv  32143  hdmaplkr  32399  hdmapip0  32401  hlhillcs  32444
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 178  df-an 361
  Copyright terms: Public domain W3C validator