Theorem biimpar 473

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

Step	Hyp	Ref	Expression
1		biimpa.1	. . 3 |- ( ph -> ( ps <-> ch ) )
2	1	biimprd 216	. 2 |- ( ph -> ( ch -> ps ) )
3	2	imp 420	1 |- ( ( ph /\ ch ) -> ps )

Syntax hints:   -> wi 4   <-> wb 178   /\ wa 360

This theorem is referenced by:  exbiri  607  bitr  691  oplem1  932  eqtr  2455  opabss  4271  euotd  4459  xpsspw  4988  brcogw  5043  somin1  5272  funfni  5547  fnco  5555  fnssres  5560  fn0  5566  fnimadisj  5567  fnimaeq0  5568  foco  5665  foimacnv  5694  fvelimab  5784  dffv2  5798  fvopab3ig  5805  dff3  5884  dffo4  5887  fnexALT  5964  f1eqcocnv  6030  isomin  6059  f1ocnv2d  6297  xp1st  6378  xp2nd  6379  iinon  6604  tfrlem1  6638  tfr3  6662  oawordri  6795  oaass  6806  omeulem1  6827  oeoa  6842  oeoe  6844  oeeulem  6846  ecelqsg  6961  elqsn0  6975  pwdom  7261  marypha1lem  7440  wofib  7516  cantnff  7631  cantnfp1  7639  cantnf  7651  cnfcomlem  7658  r1sscl  7713  rankval3b  7754  infxpidm2  7900  numdom  7921  onssnum  7923  acni  7928  acni2  7929  dfac5  8011  cdalepw  8078  infunsdom1  8095  infunsdom  8096  cofsmo  8151  cfsmolem  8152  fin1ai  8175  fin2i  8177  isf34lem1  8254  fin67  8277  itunisuc  8301  axdc3lem4  8335  zornn0g  8387  ttukeylem6  8396  brdom3  8408  tsken  8631  tskcard  8658  r1tskina  8659  intgru  8691  prlem934  8912  ltexprlem7  8921  uzindOLD  10366  xrmaxeq  10769  xrmineq  10770  xmulneg1  10850  ixxun  10934  fzm1  11129  elfznelfzo  11194  btwnzge0  11232  ioopnfsup  11247  icopnfsup  11248  faclbnd4lem4  11589  hasheni  11634  hashgt0  11664  hashge1  11665  hashprb  11670  lennncl  11738  ccatlid  11750  ccatass  11752  swrdid  11774  ccatswrd  11775  swrdccat2  11777  revccat  11800  cnpart  12047  resqreu  12060  recval  12128  abs1m  12141  abslem2  12145  fzomaxdiflem  12148  sqreulem  12165  sqreu  12166  limsupgre  12277  rlimdiv  12441  fsumparts  12587  climcnds  12633  expcnv  12645  ndvdssub  12929  sadcaddlem  12971  rplpwr  13058  dvdssqlem  13061  algcvgblem  13070  eucalgcvga  13079  coprimeprodsq  13185  pythagtriplem11  13201  pythagtriplem13  13203  pcadd2  13261  4sqlem11  13325  vdwlem6  13356  vdwlem8  13358  vdwlem10  13360  ramval  13378  ramcl2  13386  ramlb  13389  ram0  13392  mreintcl  13822  mrcval  13837  mrccl  13838  mrcuni  13848  mrcun  13849  acsfiel  13881  rescabs  14035  funcres  14095  setcmon  14244  setcepi  14245  yonffthlem  14381  pleval2i  14423  pospo  14432  poslubdg  14577  acsdrsel  14595  acsdrscl  14598  acsficl  14599  psss  14648  grpidd  14720  ismndd  14721  gsumccat  14789  gsumwmhm  14792  subgmulg  14960  resghm  15024  conjnsg  15043  lsmelvalix  15277  pj1ghm  15337  efgredlemc  15379  frgp0  15394  divsabl  15482  cycsubgcyg  15512  gsumval3  15516  gsumcllem  15518  ablfac1c  15631  pgpfac1lem5  15639  isrngd  15700  lspsneq0b  16091  lmodindp1  16092  lmhmf1o  16124  lmhmpreima  16126  reslmhm  16130  lspsncmp  16190  lspsneq  16196  znf1o  16834  uniopn  16972  ntrval  17102  clsval  17103  neival  17168  neiptopreu  17199  lpval  17205  restdis  17244  lmbrf  17326  cnpnei  17330  1stcrest  17518  hauspwdom  17566  txcnpi  17642  ptrescn  17673  xkococnlem  17693  qtopeu  17750  kqreglem1  17775  ptuncnv  17841  filss  17887  fsubbas  17901  fbasrn  17918  cfinfil  17927  ufinffr  17963  elfm3  17984  rnelfmlem  17986  rnelfm  17987  flimclslem  18018  flfval  18024  isfcf  18068  cnextfvval  18098  cnextf  18099  cnextcn  18100  ustelimasn  18254  trust  18261  restutop  18269  ustuqtop2  18274  utop2nei  18282  ucncn  18317  trcfilu  18326  cnextucn  18335  met1stc  18553  metustexhalfOLD  18595  metustexhalf  18596  cfilucfilOLD  18601  cfilucfil  18602  metutopOLD  18614  psmetutop  18615  nmoix  18765  nmoeq0  18772  idnghm  18779  blcvx  18831  xrsxmet  18842  iccntr  18854  icccmp  18858  iihalf1  18958  iihalf2  18960  xrhmeo  18973  cnheibor  18982  ipcau2  19193  lmmbrf  19217  iscauf  19235  cmetcaulem  19243  bcthlem4  19282  cmetcuspOLD  19309  cmetcusp  19310  minveclem4  19335  evthicc2  19359  cniccbdd  19360  ovollb2  19387  ovolunlem1a  19394  ovolunlem1  19395  voliun  19450  icombl  19460  ioombl  19461  iccvolcl  19463  mbfss  19540  mbfposb  19547  itg2const2  19635  itg2splitlem  19642  itg2gt0  19654  iblss2  19699  itgioo  19709  dvaddf  19830  dvmulf  19831  dvcobr  19834  dvcof  19836  rolle  19876  dvlip  19879  c1lip1  19883  dvivthlem1  19894  lhop1lem  19899  dvfsumlem1  19912  ftc1lem4  19925  ftc1lem5  19926  mpfind  19967  ply1divmo  20060  coe1termlem  20178  plydiveu  20217  taylplem1  20281  pserulm  20340  abelth  20359  abscxp2  20586  abscxpbnd  20639  ang180lem2  20654  ang180lem3  20655  isosctrlem1  20664  angpieqvd  20674  atandmtan  20762  birthdaylem3  20794  wilthlem2  20854  isppw  20899  isppw2  20900  dvdsflsumcom  20975  chteq0  20995  perfectlem2  21016  dchrval  21020  dchrinvcl  21039  dchrptlem1  21050  bposlem3  21072  lgsmod  21107  lgsdilem  21108  lgsdir2lem2  21110  lgsdir2  21114  lgsne0  21119  lgseisenlem1  21135  2sqlem4  21153  chpo1ubb  21177  dchrisumn0  21217  pntrsumbnd2  21263  ostthlem1  21323  ostth3  21334  uvtxnbgravtx  21506  gxcom  21859  resgrprn  21870  ghablo  21959  nvss  22074  sspn  22237  nmoub3i  22276  nmblolbii  22302  blocnilem  22307  minvecolem4  22384  htthlem  22422  norm1  22753  norm1exi  22754  pjeq  22903  axpjpj  22924  normcan  23080  pjoi0  23221  nmopub2tALT  23414  nmfnleub2  23431  eighmorth  23469  nmbdoplbi  23529  nmcoplbi  23533  nmophmi  23536  nmbdfnlbi  23554  nmcfnlbi  23557  riesz3i  23567  cnlnadjlem7  23578  branmfn  23610  nmopleid  23644  hstle  23735  superpos  23859  cvexchlem  23873  elabreximd  23993  f1o3d  24043  funcnvmptOLD  24084  funcnvmpt  24085  xrofsup  24128  eliccelico  24142  elicoelioo  24143  iocinif  24146  difioo  24147  eliccioo  24179  subofld  24247  unitdivcld  24301  tpr2rico  24312  lmxrge0  24339  elzrhunit  24365  qqhf  24372  indf1ofs  24425  gsumesum  24453  esumfsup  24462  esumcvg  24478  issgon  24508  sigainb  24521  insiga  24522  isrnmeas  24556  measvunilem  24568  volmeas  24589  imambfm  24614  probun  24679  dstfrvunirn  24734  derangen  24860  subfacp1lem2b  24869  subfacp1lem4  24871  subfacp1lem5  24872  derangfmla  24878  ptpcon  24922  ntrivcvg  25227  wfr3g  25539  wfrlem3  25542  wfrlem4  25543  wsuclem  25578  frr3g  25583  frrlem3  25586  nocvxmin  25648  nobndlem6  25654  nobndup  25657  nobnddown  25658  brcgr  25841  colinearalglem4  25850  colinearalg  25851  axlowdimlem14  25896  axcontlem4  25908  colinearex  25996  btwnconn1lem11  26033  btwnconn1lem12  26034  supaddc  26239  mblfinlem2  26246  voliunnfl  26252  mbfresfi  26255  itg2addnclem  26258  itg2addnclem3  26260  itg2gt0cn  26262  ftc1cnnclem  26280  ftc1anclem5  26286  gtinf  26324  nn0prpwlem  26327  lfinpfin  26385  cover2  26417  indexdom  26438  sdclem1  26449  fdc  26451  equivbnd2  26503  heiborlem8  26529  heibor  26532  isdrngo2  26576  iscringd  26611  smprngopr  26664  prnc  26679  nacsfix  26768  3rexfrabdioph  26859  4rexfrabdioph  26860  6rexfrabdioph  26861  7rexfrabdioph  26862  eldioph4b  26874  pellexlem2  26895  pellexlem5  26898  expmordi  27012  jm2.26lem3  27074  pwssplit3  27169  dsmmlss  27189  frlmlbs  27228  frlmup1  27229  numinfctb  27247  f1otrspeq  27369  pmtrval  27373  pmtrrn  27378  pmtrfinv  27381  psgnunilem1  27395  psgnunilem5  27396  psgnunilem4  27399  psgneldm2i  27407  mat1  27461  dvconstbi  27530  ioovolcl  27720  stoweidlem27  27754  stoweidlem28  27755  ltdifltdiv  28159  modifeq2int  28172  swrdltnd  28203  swrdnd  28204  swrdvalodmlem1  28209  swrdvalodm2  28210  swrdccat  28238  cshwidx  28264  swrdtrcfvl  28287  frghash2spot  28514  onetansqsecsq  28566  cotsqcscsq  28567  elpwgded  28713  elpwgdedVD  29091  sspwimpcf  29094  sspwimpcfVD  29095  sspwimpALT2  29102  a9e2ndeqALT  29105  bnj529  29171  bnj548  29330  bnj570  29338  bnj852  29354  bnj929  29369  bnj1097  29412  bnj1118  29415  bnj1145  29424  islfld  29922  lkrshpor  29967  lfl1dim  29981  lfl1dim2N  29982  cmtcomlemN  30108  2lplnmN  30418  pmapjat1  30712  trlnid  31038  tendoex  31834  dia1dimid  31923  dibval2  32004  dihmeetlem2N  32159  dochlkr  32245  mapdcv  32520  hdmaplkr  32776  hdmapip0  32778  hlhillcs  32821

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 179  df-an 362