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

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

Syntax hints:   -> wi 4   <-> wb 177   /\ wa 359

This theorem is referenced by:  exbiri  606  bitr  690  oplem1  931  eqtr  2425  opabss  4233  euotd  4421  xpsspw  4949  brcogw  5004  somin1  5233  funfni  5508  fnco  5516  fnssres  5521  fn0  5527  fnimadisj  5528  fnimaeq0  5529  foco  5626  foimacnv  5655  fvelimab  5745  dffv2  5759  fvopab3ig  5766  dff3  5845  dffo4  5848  fnexALT  5925  f1eqcocnv  5991  isomin  6020  f1ocnv2d  6258  xp1st  6339  xp2nd  6340  iinon  6565  tfrlem1  6599  tfr3  6623  oawordri  6756  oaass  6767  omeulem1  6788  oeoa  6803  oeoe  6805  oeeulem  6807  ecelqsg  6922  elqsn0  6936  pwdom  7222  marypha1lem  7400  wofib  7474  cantnff  7589  cantnfp1  7597  cantnf  7609  cnfcomlem  7616  r1sscl  7671  rankval3b  7712  infxpidm2  7858  numdom  7879  onssnum  7881  acni  7886  acni2  7887  dfac5  7969  cdalepw  8036  infunsdom1  8053  infunsdom  8054  cofsmo  8109  cfsmolem  8110  fin1ai  8133  fin2i  8135  isf34lem1  8212  fin67  8235  itunisuc  8259  axdc3lem4  8293  zornn0g  8345  ttukeylem6  8354  brdom3  8366  tsken  8589  tskcard  8616  r1tskina  8617  intgru  8649  prlem934  8870  ltexprlem7  8879  uzindOLD  10324  xrmaxeq  10727  xrmineq  10728  xmulneg1  10808  ixxun  10892  fzm1  11086  elfznelfzo  11151  btwnzge0  11189  ioopnfsup  11204  icopnfsup  11205  faclbnd4lem4  11546  hasheni  11591  hashgt0  11621  hashge1  11622  hashprb  11627  lennncl  11695  ccatlid  11707  ccatass  11709  swrdid  11731  ccatswrd  11732  swrdccat2  11734  revccat  11757  cnpart  12004  resqreu  12017  recval  12085  abs1m  12098  abslem2  12102  fzomaxdiflem  12105  sqreulem  12122  sqreu  12123  limsupgre  12234  rlimdiv  12398  fsumparts  12544  climcnds  12590  expcnv  12602  ndvdssub  12886  sadcaddlem  12928  rplpwr  13015  dvdssqlem  13018  algcvgblem  13027  eucalgcvga  13036  coprimeprodsq  13142  pythagtriplem11  13158  pythagtriplem13  13160  pcadd2  13218  4sqlem11  13282  vdwlem6  13313  vdwlem8  13315  vdwlem10  13317  ramval  13335  ramcl2  13343  ramlb  13346  ram0  13349  mreintcl  13779  mrcval  13794  mrccl  13795  mrcuni  13805  mrcun  13806  acsfiel  13838  rescabs  13992  funcres  14052  setcmon  14201  setcepi  14202  yonffthlem  14338  pleval2i  14380  pospo  14389  poslubdg  14534  acsdrsel  14552  acsdrscl  14555  acsficl  14556  psss  14605  grpidd  14677  ismndd  14678  gsumccat  14746  gsumwmhm  14749  subgmulg  14917  resghm  14981  conjnsg  15000  lsmelvalix  15234  pj1ghm  15294  efgredlemc  15336  frgp0  15351  divsabl  15439  cycsubgcyg  15469  gsumval3  15473  gsumcllem  15475  ablfac1c  15588  pgpfac1lem5  15596  isrngd  15657  lspsneq0b  16048  lmodindp1  16049  lmhmf1o  16081  lmhmpreima  16083  reslmhm  16087  lspsncmp  16147  lspsneq  16153  znf1o  16791  uniopn  16929  ntrval  17059  clsval  17060  neival  17125  neiptopreu  17156  lpval  17162  restdis  17200  lmbrf  17282  cnpnei  17286  1stcrest  17473  hauspwdom  17521  txcnpi  17597  ptrescn  17628  xkococnlem  17648  qtopeu  17705  kqreglem1  17730  ptuncnv  17796  filss  17842  fsubbas  17856  fbasrn  17873  cfinfil  17882  ufinffr  17918  elfm3  17939  rnelfmlem  17941  rnelfm  17942  flimclslem  17973  flfval  17979  isfcf  18023  cnextfvval  18053  cnextf  18054  cnextcn  18055  ustelimasn  18209  trust  18216  restutop  18224  ustuqtop2  18229  utop2nei  18237  ucncn  18272  trcfilu  18281  cnextucn  18290  met1stc  18508  metustexhalfOLD  18550  metustexhalf  18551  cfilucfilOLD  18556  cfilucfil  18557  metutopOLD  18569  psmetutop  18570  nmoix  18720  nmoeq0  18727  idnghm  18734  blcvx  18786  xrsxmet  18797  iccntr  18809  icccmp  18813  iihalf1  18913  iihalf2  18915  xrhmeo  18928  cnheibor  18937  ipcau2  19148  lmmbrf  19172  iscauf  19190  cmetcaulem  19198  bcthlem4  19237  cmetcuspOLD  19264  cmetcusp  19265  minveclem4  19290  evthicc2  19314  cniccbdd  19315  ovollb2  19342  ovolunlem1a  19349  ovolunlem1  19350  voliun  19405  icombl  19415  ioombl  19416  iccvolcl  19418  mbfss  19495  mbfposb  19502  itg2const2  19590  itg2splitlem  19597  itg2gt0  19609  iblss2  19654  itgioo  19664  dvaddf  19785  dvmulf  19786  dvcobr  19789  dvcof  19791  rolle  19831  dvlip  19834  c1lip1  19838  dvivthlem1  19849  lhop1lem  19854  dvfsumlem1  19867  ftc1lem4  19880  ftc1lem5  19881  mpfind  19922  ply1divmo  20015  coe1termlem  20133  plydiveu  20172  taylplem1  20236  pserulm  20295  abelth  20314  abscxp2  20541  abscxpbnd  20594  ang180lem2  20609  ang180lem3  20610  isosctrlem1  20619  angpieqvd  20629  atandmtan  20717  birthdaylem3  20749  wilthlem2  20809  isppw  20854  isppw2  20855  dvdsflsumcom  20930  chteq0  20950  perfectlem2  20971  dchrval  20975  dchrinvcl  20994  dchrptlem1  21005  bposlem3  21027  lgsmod  21062  lgsdilem  21063  lgsdir2lem2  21065  lgsdir2  21069  lgsne0  21074  lgseisenlem1  21090  2sqlem4  21108  chpo1ubb  21132  dchrisumn0  21172  pntrsumbnd2  21218  ostthlem1  21278  ostth3  21289  uvtxnbgravtx  21461  gxcom  21814  resgrprn  21825  ghablo  21914  nvss  22029  sspn  22192  nmoub3i  22231  nmblolbii  22257  blocnilem  22262  minvecolem4  22339  htthlem  22377  norm1  22708  norm1exi  22709  pjeq  22858  axpjpj  22879  normcan  23035  pjoi0  23176  nmopub2tALT  23369  nmfnleub2  23386  eighmorth  23424  nmbdoplbi  23484  nmcoplbi  23488  nmophmi  23491  nmbdfnlbi  23509  nmcfnlbi  23512  riesz3i  23522  cnlnadjlem7  23533  branmfn  23565  nmopleid  23599  hstle  23690  superpos  23814  cvexchlem  23828  elabreximd  23948  f1o3d  23998  funcnvmptOLD  24039  funcnvmpt  24040  xrofsup  24083  eliccelico  24097  elicoelioo  24098  iocinif  24101  difioo  24102  eliccioo  24134  subofld  24202  unitdivcld  24256  tpr2rico  24267  lmxrge0  24294  elzrhunit  24320  qqhf  24327  indf1ofs  24380  gsumesum  24408  esumfsup  24417  esumcvg  24433  issgon  24463  sigainb  24476  insiga  24477  isrnmeas  24511  measvunilem  24523  volmeas  24544  imambfm  24569  probun  24634  dstfrvunirn  24689  derangen  24815  subfacp1lem2b  24824  subfacp1lem4  24826  subfacp1lem5  24827  derangfmla  24833  ptpcon  24877  ntrivcvg  25182  wfr3g  25473  wfrlem3  25476  wfrlem4  25477  frr3g  25498  frrlem3  25501  nocvxmin  25563  nobndlem6  25569  nobndup  25572  nobnddown  25573  brcgr  25747  colinearalglem4  25756  colinearalg  25757  axlowdimlem14  25802  axcontlem4  25814  colinearex  25902  btwnconn1lem11  25939  btwnconn1lem12  25940  supaddc  26141  mblfinlem  26147  voliunnfl  26153  mbfresfi  26156  itg2addnclem  26159  itg2addnclem3  26161  itg2gt0cn  26163  ftc1cnnclem  26181  gtinf  26216  nn0prpwlem  26219  lfinpfin  26277  cover2  26309  indexdom  26330  sdclem1  26341  fdc  26343  equivbnd2  26395  heiborlem8  26421  heibor  26424  isdrngo2  26468  iscringd  26503  smprngopr  26556  prnc  26571  nacsfix  26660  3rexfrabdioph  26751  4rexfrabdioph  26752  6rexfrabdioph  26753  7rexfrabdioph  26754  eldioph4b  26766  pellexlem2  26787  pellexlem5  26790  expmordi  26904  jm2.26lem3  26966  pwssplit3  27062  dsmmlss  27082  frlmlbs  27121  frlmup1  27122  numinfctb  27140  f1otrspeq  27262  pmtrval  27266  pmtrrn  27271  pmtrfinv  27274  psgnunilem1  27288  psgnunilem5  27289  psgnunilem4  27292  psgneldm2i  27300  mat1  27354  dvconstbi  27423  ioovolcl  27613  stoweidlem27  27647  stoweidlem28  27648  swrdltnd  28004  swrdnd  28005  frghash2spot  28170  onetansqsecsq  28222  cotsqcscsq  28223  elpwgded  28366  elpwgdedVD  28742  sspwimpcf  28745  sspwimpcfVD  28746  sspwimpALT2  28754  a9e2ndeqALT  28757  bnj529  28819  bnj548  28978  bnj570  28986  bnj852  29002  bnj929  29017  bnj1097  29060  bnj1118  29063  bnj1145  29072  islfld  29549  lkrshpor  29594  lfl1dim  29608  lfl1dim2N  29609  cmtcomlemN  29735  2lplnmN  30045  pmapjat1  30339  trlnid  30665  tendoex  31461  dia1dimid  31550  dibval2  31631  dihmeetlem2N  31786  dochlkr  31872  mapdcv  32147  hdmaplkr  32403  hdmapip0  32405  hlhillcs  32448

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