Theorem biimpa 501

Description: Importation inference from a logical equivalence. (Contributed by NM, 3-May-1994.)

Hypothesis

Ref	Expression
biimpa.1	|- ( ph -> ( ps <-> ch ) )

Assertion

Ref	Expression
biimpa	|- ( ( ph /\ ps ) -> ch )

Proof of Theorem biimpa

Step	Hyp	Ref	Expression
1		biimpa.1	. . 3 |- ( ph -> ( ps <-> ch ) )
2	1	biimpd 219	. 2 |- ( ph -> ( ps -> ch ) )
3	2	imp 445	1 |- ( ( ph /\ ps ) -> ch )

Syntax hints:   -> wi 4   <-> wb 196   /\ wa 384

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 197  df-an 386

This theorem is referenced by:  simprbda  653  simplbda  654  pm5.1  902  bimsc1  980  biimp3a  1432  equsex  2292  euor  2512  euan  2530  cgsexg  3238  cgsex2g  3239  cgsex4g  3240  ceqsex  3241  sbciegft  3466  sbeqalb  3488  syl5sseq  3653  elpwunsn  4224  ralxfr2d  4882  propeqop  4970  euotd  4975  relop  5272  elsnxp  5677  sspred  5688  fnbr  5993  f1o00  6171  foelrni  6244  dffv2  6271  iinpreima  6345  funressn  6426  fnex  6481  f1prex  6539  weniso  6604  riotaeqimp  6634  f1ocnv2d  6886  ofrval  6907  limsssuc  7050  resiexg  7102  eloprabi  7232  1stconst  7265  2ndconst  7266  frxp  7287  poxp  7289  smodm2  7452  smoiso  7459  tz7.44lem1  7501  oev2  7603  oesuclem  7605  oecl  7617  omordi  7646  omwordri  7652  omword2  7654  omordlim  7657  omlimcl  7658  omeulem2  7663  oeordi  7667  oewordri  7672  oelim2  7675  oeoa  7677  oeoe  7679  nnawordi  7701  nnaordex  7718  erth  7791  iiner  7819  pw2f1olem  8064  pw2f1o  8065  onomeneq  8150  onfin2  8152  unxpdomlem2  8165  isinf  8173  findcard2  8200  fipreima  8272  fipwss  8335  cantnfp1lem3  8577  carden2b  8793  carddomi2  8796  infxpenlem  8836  acni2  8869  numacn  8872  alephfp  8931  pwsdompw  9026  ackbij2lem3  9063  cfeq0  9078  cfsuc  9079  cfsmolem  9092  domfin4  9133  axdc3lem2  9273  axdc3lem4  9275  alephreg  9404  fpwwe2  9465  winainflem  9515  r1limwun  9558  inar1  9597  grudomon  9639  nlt1pi  9728  indpi  9729  nqereu  9751  ltbtwnnq  9800  prlem934  9855  prlem936  9869  addgt0sr  9925  leltne  10127  ne0gt0  10142  mullt0  10547  msqgt0  10548  mulne0  10669  divne0  10697  div2neg  10748  ltmul12a  10879  recgt1i  10920  negfi  10971  nn2ge  11045  div4p1lem1div2  11287  nn0lt2  11440  peano5uzi  11466  eluzp1m1  11711  eluzaddi  11714  eluzsubi  11715  uz2m1nn  11763  nn01to3  11781  rpnnen1lem5  11818  rpnnen1lem5OLD  11824  rphalflt  11860  xrleltne  11978  max0sub  12027  xmulpnf1n  12108  xmulge0  12114  xadddi  12125  supxr  12143  supxr2  12144  ixxdisj  12190  ixxun  12191  ixxub  12196  ixxlb  12197  iccgelb  12230  icodisj  12297  difreicc  12304  iccf1o  12316  fzsuc2  12398  fzonmapblen  12513  elfznelfzo  12573  flge0nn0  12621  flge1nn  12622  2submod  12731  modfzo0difsn  12742  seqf1olem2  12841  expubnd  12921  sqlecan  12971  bernneq  12990  bernneq2  12991  expnbnd  12993  discr1  13000  facwordi  13076  faclbnd4lem4  13083  bcpasc  13108  hashgt0n0  13156  elprchashprn2  13184  hash1to3  13273  iswrdi  13309  ffz0iswrd  13332  ccatsymb  13366  ccatass  13371  swrdlend  13431  swrdfv2  13446  swrdspsleq  13449  swrdswrdlem  13459  swrdswrd  13460  swrdswrd0  13462  swrdccatin12lem2b  13486  revccat  13515  revrev  13516  repswccat  13532  2cshw  13559  cshwcsh2id  13574  revco  13580  cshco  13582  s2f1o  13661  s4f1o  13663  wrdlen2i  13686  wwlktovf  13699  ofccat  13708  trclub  13739  sqr0lem  13981  sqrlem2  13984  sqrlem7  13989  max0add  14050  recval  14062  nnabscl  14065  absmax  14069  sqreulem  14099  climi0  14243  lo1bdd2  14255  rlimresb  14296  lo1eq  14299  rlimeq  14300  isercolllem3  14397  climsup  14400  fsumsplit  14471  fsumcom2  14505  fsumcom2OLD  14506  explecnv  14597  fprodser  14679  fprodsplit  14696  fprodcom2  14714  fprodcom2OLD  14715  eftlub  14839  sin02gt0  14922  rpnnen2lem10  14952  dvdsleabs2  15034  mulmoddvds  15051  odd2np1  15065  oexpneg  15069  sqoddm1div8z  15078  bitsf1  15168  sadcaddlem  15179  bitsuz  15196  rplpwr  15276  rppwr  15277  nn0seqcvgd  15283  lcmneg  15316  qredeq  15371  dvdsnprmd  15403  oddprmge3  15412  isprm7  15420  qgt0numnn  15459  phibndlem  15475  hashgcdeq  15494  reumodprminv  15509  coprimeprodsq2  15514  pythagtrip  15539  dvdsprmpweqle  15590  fldivp1  15601  unbenlem  15612  4sqlem9  15650  4sqlem15  15663  4sqlem16  15664  vdwlem6  15690  vdwlem10  15694  vdwlem11  15695  vdwlem13  15697  vdw  15698  prmgaplem7  15761  prmgaplem8  15762  cshwshashlem1  15802  mreuni  16260  cidpropd  16370  subsubc  16513  ffthiso  16589  fuciso  16635  setcmon  16737  setcepi  16738  catciso  16757  funcestrcsetclem7  16786  funcestrcsetclem8  16787  setc1strwun  16793  funcsetcestrclem7  16801  hofcl  16899  hofpropd  16907  yonedalem4c  16917  yonedainv  16921  issstrmgm  17252  imasmnd  17328  pwsco1mhm  17370  imasgrp  17531  subginv  17601  subgmulg  17608  eqger  17644  subgga  17733  orbstafun  17744  orbsta  17746  symggrp  17820  psgnsn  17940  dfod2  17981  gexval  17993  gex1  18006  sylow2blem1  18035  sylow3lem1  18042  pj1eu  18109  efgredlema  18153  frgp0  18173  frgpmhm  18178  odadd1  18251  0cyg  18294  gsumzres  18310  gsumzsplit  18327  gsummptfzcl  18368  dprd2dlem1  18440  dprd2da  18441  dmdprdsplit2  18445  dprdsplit  18447  pgpfaclem3  18482  ablfac2  18488  imasring  18619  rhmf1o  18732  kerf1hrm  18743  subrg1  18790  abvneg  18834  lmhmf1o  19046  lmhmima  19047  reslmhm2b  19054  pwssplit0  19058  pwssplit1  19059  lsmspsn  19084  lspdisj  19125  lidlmcl  19217  isnzr2hash  19264  fidomndrnglem  19306  mplsubglem  19434  mplmonmul  19464  mplbas2  19470  subrgascl  19498  subrgasclcl  19499  evlsval2  19520  mpfind  19536  lply1binomsc  19677  absabv  19803  f1lindf  20161  mat0dimscm  20275  scmataddcl  20322  scmatsubcl  20323  smatvscl  20330  mdetunilem8  20425  chfacfscmul0  20663  chfacfscmulfsupp  20664  chfacfscmulgsum  20665  chfacfpmmul0  20667  chfacfpmmulfsupp  20668  chfacfpmmulgsum  20669  cpmidpmatlem3  20677  chcoeffeqlem  20690  cayleyhamilton0  20694  cayleyhamiltonALT  20696  cayleyhamilton1  20697  elcls  20877  clsndisj  20879  isclo2  20892  neiuni  20926  neissex  20931  neiptopreu  20937  tgrest  20963  neitr  20984  tgcnp  21057  lmfpm  21099  lmcl  21101  lmss  21102  lmff  21105  ist1-2  21151  cnt1  21154  cmpsublem  21202  clsconn  21233  locfindis  21333  kgeni  21340  kgenidm  21350  txcnpi  21411  ptpjopn  21415  ptclsg  21418  txcmplem1  21444  qtoptop2  21502  qtoptopon  21507  r0sep  21551  ptunhmeo  21611  t0kq  21621  fsubbas  21671  neifil  21684  uffixsn  21729  ufildr  21735  rnelfm  21757  isfcls2  21817  uffclsflim  21835  alexsublem  21848  cnextfun  21868  cnextfvval  21869  cnextf  21870  cnextcn  21871  tmdcn2  21893  symgtgp  21905  tsmssplit  21955  ustuni  22030  trust  22033  utoptop  22038  restutop  22041  restutopopn  22042  ustuqtop1  22045  ustuqtop2  22046  ustuqtop3  22047  ustuqtop4  22048  utop2nei  22054  utop3cls  22055  ucncn  22089  trcfilu  22098  cfiluweak  22099  psmetdmdm  22110  xmeter  22238  prdsbl  22296  neibl  22306  methaus  22325  prdsxmslem2  22334  metustto  22358  metustexhalf  22361  metust  22363  cfilucfil  22364  psmetutop  22372  tngngp2  22456  tngngp  22458  tgqioo  22603  xrsxmet  22612  icccmplem1  22625  icccmplem2  22626  cnmpt2pc  22727  iihalf2  22732  icoopnst  22738  iocopnst  22739  xrhmeo  22745  lebnumlem1  22760  lebnumlem3  22762  pi1blem  22839  pi1grplem  22849  pi1xfrf  22853  pi1xfr  22855  pi1xfrcnvlem  22856  pi1cof  22859  pi1coghm  22861  cmetcaulem  23086  causs  23096  metcld  23104  lmcau  23111  rrxcph  23180  minveclem4  23203  ivthlem2  23221  ivthlem3  23222  ivthicc  23227  ovolshftlem1  23277  ovolicc1  23284  ovolicopnf  23292  volfiniun  23315  uniioombllem3  23353  dyaddisjlem  23363  vitalilem2  23378  itg1ge0  23453  mbfi1fseqlem3  23484  xrge0f  23498  itg2seq  23509  itg2monolem1  23517  itg2addlem  23525  itg2gt0  23527  iblcnlem  23555  itgss3  23581  itgsplit  23602  dvnff  23686  dvferm2  23750  dvlip2  23758  dveq0  23763  dvge0  23769  dvcnvre  23782  dvfsumle  23784  dvfsumabs  23786  dvfsumlem2  23790  ftc1lem2  23799  ftc1lem4  23802  ftc1lem5  23803  ftc1cn  23806  ftc2  23807  itgsubstlem  23811  coe1mul3  23859  ply1divex  23896  dgrlem  23985  dgrlb  23992  coemulhi  24010  dgrlt  24022  dgrmul  24026  plydivlem4  24051  fta1  24063  aaliou2b  24096  taylplem2  24118  dvtaylp  24124  ulmcau  24149  tanabsge  24258  sinq12gt0  24259  argimgt0  24358  cxplea  24442  cxple2  24443  cxpsqrt  24449  cxpaddlelem  24492  loglesqrt  24499  logrec  24501  ang180lem2  24540  lawcos  24546  asinlem3a  24597  asinlem3  24598  asinsin  24619  atanlogaddlem  24640  atanlogadd  24641  atanlogsub  24643  atantan  24650  atanbnd  24653  atantayl2  24665  efrlim  24696  wilthlem2  24795  basellem2  24808  sqfpc  24863  ppieq0  24902  sqff1o  24908  fsumdvdscom  24911  ppiub  24929  chpeq0  24933  chtleppi  24935  fsumvma  24938  fsumvma2  24939  mersenne  24952  dchrabs2  24987  dchr1re  24988  dchrpt  24992  lgsdilem  25049  lgsdinn0  25070  gausslemma2dlem0b  25082  gausslemma2dlem1a  25090  gausslemma2dlem5  25096  gausslemma2dlem6  25097  lgsquad3  25112  m1lgs  25113  2lgslem1a  25116  2lgslem1  25119  2lgslem3a1  25125  2lgslem3b1  25126  2lgslem3c1  25127  2lgslem3d1  25128  2sqlem6  25148  rpvmasumlem  25176  dchrisumlem3  25180  dchrisum0flblem1  25197  pntibndlem2a  25279  pntlem3  25298  padicabv  25319  ercgrg  25412  tglnunirn  25443  tglineeltr  25526  mirln2  25572  mirbtwnhl  25575  isperp2  25610  outpasch  25647  lnopp2hpgb  25655  ttgbtwnid  25764  axcontlem2  25845  axcontlem12  25855  upgredg  26032  fusgrfisstep  26221  nbupgrres  26266  usgrnbcnvfv  26267  nbusgredgeu  26268  nbcplgr  26330  cusgrexi  26339  cusgrsizeinds  26348  vtxdgoddnumeven  26449  uhgr0edg0rgr  26469  wlkl1loop  26534  upgriswlk  26537  usgr2pthlem  26659  cyclnspth  26695  wspthnp  26737  elwwlks2ons3  26848  elwspths2on  26853  usgr2wspthons3  26857  clwlkclwwlklem2a4  26898  clwlkclwwlk2  26904  clwwlksn1loop  26909  clwwlksf1  26917  clwwisshclwws  26928  eleclclwwlksnlem2  26939  clwlksfclwwlk2wrd  26958  clwlksf1clwwlklem3  26967  clwlksf1clwwlklem  26968  1pthon2v  27013  upgr3v3e3cycl  27040  upgreupthi  27068  eupth2lemb  27097  frgrncvvdeqlem7  27169  frgrncvvdeqlem8  27170  frgrncvvdeqlem9  27171  numclwwlkovf2ex  27219  numclwwlk2lem1  27235  frgrreggt1  27251  frgrregord013  27253  cnnv  27532  nmounbseqi  27632  nmounbseqiALT  27633  nmlnogt0  27652  nmblolbii  27654  blocnilem  27659  ajmoi  27714  minvecolem4  27736  hhnv  28022  norm1  28106  hhssnv  28121  pjhtheu  28253  pjpreeq  28257  spanunsni  28438  fh1  28477  fh2  28478  cm2j  28479  chscllem4  28499  pjid  28554  adjmo  28691  eleigveccl  28818  eigvalcl  28820  eigvec1  28821  eighmre  28822  eighmorth  28823  nmop0h  28850  nmbdoplbi  28883  nmcoplbi  28887  nmophmi  28890  lncnopbd  28896  nmbdfnlbi  28908  nmcfnlbi  28911  cnlnadjeui  28936  branmfn  28964  rnbra  28966  nmopleid  28998  strlem5  29114  hstrlem5  29122  dmdbr3  29164  dmdbr4  29165  mdsl3  29175  hatomistici  29221  cvexchlem  29227  chirredlem1  29249  chirredlem2  29250  chirredi  29253  atcvat3i  29255  atcvat4i  29256  atabsi  29260  mdsymlem1  29262  mdsymlem3  29264  mdsymlem5  29266  dmdbr5ati  29281  cdj1i  29292  foresf1o  29343  rabfodom  29344  elabreximd  29348  elpreq  29360  f1o3d  29431  acunirnmpt2f  29461  disjdsct  29480  1stpreimas  29483  fcobij  29500  fpwrelmapffslem  29507  nn0sqeq1  29513  xrofsup  29533  eliccelico  29539  elicoelioo  29540  numdenneg  29563  fsumiunle  29575  dpadd3  29620  threehalves  29623  xrge0addgt0  29691  xrge0adddir  29692  xrge0npcan  29694  omndmul3  29713  submarchi  29740  archirng  29742  archirngz  29743  archiexdiv  29744  archiabllem1a  29745  1smat1  29870  madjusmdetlem2  29894  locfinreflem  29907  metideq  29936  unitdivcld  29947  cnre2csqlem  29956  ordtconnlem1  29970  fmcncfil  29977  lmxrge0  29998  pl1cn  30001  zrhunitpreima  30022  elzdif0  30024  qqhval2lem  30025  qqhf  30030  indf1ofs  30088  esumfsup  30132  esumpcvgval  30140  esum2dlem  30154  esum2d  30155  esumiun  30156  sigasspw  30179  issgon  30186  ispisys2  30216  meascnbl  30282  voliune  30292  volfiniune  30293  omssubaddlem  30361  carsggect  30380  carsgclctunlem2  30381  oddpwdc  30416  eulerpartlems  30422  eulerpartlemgvv  30438  ballotlemfrcn0  30591  sgncl  30600  sgnneg  30602  sgn3da  30603  sgnmul  30604  sgnsub  30606  gsumnunsn  30615  signsplypnf  30627  signsply0  30628  signslema  30639  signstfvneq0  30649  signsvfpn  30662  signsvfnn  30663  repr0  30689  reprlt  30697  reprgt  30699  reprinfz1  30700  chtvalz  30707  breprexplemc  30710  hgt750lemb  30734  hgt750leme  30736  bnj563  30813  bnj1001  31028  subfacp1lem5  31166  subfacp1lem6  31167  erdszelem9  31181  ptpconn  31215  resconn  31228  cvmlift3lem7  31307  msrrcl  31440  trpredrec  31738  scutbdaylt  31922  btwnintr  32126  btwnouttr  32131  cgrxfr  32162  btwnconn1lem12  32205  colinbtwnle  32225  lineelsb2  32255  nn0prpwlem  32317  neibastop3  32357  onintopssconn  32439  bj-restsnss  33036  bj-restsnss2  33037  taupilem1  33167  relowlssretop  33211  finxpsuclem  33234  unccur  33392  lindsenlbs  33404  matunitlindflem1  33405  matunitlindflem2  33406  poimirlem2  33411  poimirlem8  33417  poimirlem14  33423  poimirlem15  33424  poimirlem17  33426  poimirlem20  33429  poimirlem22  33431  poimirlem24  33433  poimirlem25  33434  poimirlem27  33436  poimirlem28  33437  poimirlem31  33440  heicant  33444  mblfinlem2  33447  itg2gt0cn  33465  itgaddnclem2  33469  ftc1cnnclem  33483  ftc1cnnc  33484  ftc1anclem2  33486  ftc1anclem5  33489  ftc1anclem7  33491  ftc1anc  33493  ftc2nc  33494  dvasin  33496  areacirclem5  33504  areacirc  33505  fdc  33541  incsequz  33544  blbnd  33586  prdstotbnd  33593  cnpwstotbnd  33596  ismtyres  33607  rngohomf  33765  rngohom1  33767  rngohomadd  33768  rngohommul  33769  idlss  33815  idl0cl  33817  idladdcl  33818  idllmulcl  33819  idlrmulcl  33820  maxidlnr  33841  maxidlmax  33842  smprngopr  33851  pridlc  33870  ac6s6f  33981  lshpnel2N  34272  islsati  34281  lkr0f  34381  lfl1dim  34408  lfl1dim2N  34409  omlfh1N  34545  leat  34580  atlatmstc  34606  cvlatexch3  34625  lnnat  34713  cvrat3  34728  cvrat4  34729  3dim3  34755  dalem4  34951  dalem39  34997  paddasslem12  35117  psubcliN  35224  pmapojoinN  35254  lhpm0atN  35315  lhprelat3N  35326  trlnid  35466  trlval3  35474  cdleme22b  35629  trljco  36028  diaglbN  36344  dibvalrel  36452  dicvalrelN  36474  diclspsn  36483  dih1dimatlem  36618  dihlatat  36626  lcfl6  36789  lcfl8  36791  lcfrvalsnN  36830  lcfrlem9  36839  mapdheq2  37018  hlhillcs  37250  hlhilhillem  37252  mzpindd  37309  lzunuz  37331  2rexfrabdioph  37360  irrapxlem3  37388  pellexlem2  37394  pellexlem5  37397  pell1234qrreccl  37418  pell14qrdich  37433  pell1qrge1  37434  elpell1qr2  37436  reglogltb  37455  reglogleb  37456  rmxycomplete  37482  2nn0ind  37510  congabseq  37541  acongrep  37547  acongeq  37550  jm2.22  37562  jm2.26lem3  37568  pw2f1ocnv  37604  limsuc2  37611  fnwe2lem3  37622  aomclem6  37629  kercvrlsm  37653  pwssplit4  37659  lpirlnr  37687  rfovcnvf1od  38298  dssmapnvod  38314  cvgdvgrat  38512  radcnvrat  38513  dvconstbi  38533  bccbc  38544  bi2imp  38688  ax6e2ndeqALT  39167  mulltgt0  39181  refsumcn  39189  cncmpmax  39191  mapdm0OLD  39383  unirnmapsn  39406  icoiccdif  39750  climinf  39838  climreeq  39845  climeldmeq  39897  coskpi2  40077  cosknegpi  40080  icccncfext  40100  dvmptfprodlem  40159  volioore  40207  stoweidlem27  40244  stoweidlem29  40246  stoweidlem31  40248  stoweidlem34  40251  stoweidlem48  40265  stoweidlem59  40276  fourierdlem109  40432  fourierswlem  40447  elaa2  40451  etransclem37  40488  hspmbllem2  40841  smflimmpt  41016  sigarcol  41053  reuan  41180  ndmaovg  41264  subsubelfzo0  41336  iccelpart  41369  fargshiftf1  41377  fargshiftfo  41378  pfxeq  41404  pfxccatin12lem1  41423  repswpfx  41436  fmtno4prmfac  41484  2pwp1prmfmtno  41504  sfprmdvdsmersenne  41520  lighneallem3  41524  proththd  41531  evenm1odd  41552  evenp1odd  41553  nnoALTV  41606  stgoldbwt  41664  sbgoldbst  41666  nnsum4primeseven  41688  nnsum4primesevenALTV  41689  bgoldbtbndlem2  41694  upgrwlkupwlk  41721  rnghmf1o  41903  rnghmsubcsetclem1  41975  zrinitorngc  42000  zrtermorngc  42001  rhmsubcsetclem1  42021  rhmsubcrngclem1  42027  funcringcsetcALTV2lem8  42043  funcringcsetclem8ALTV  42066  zrtermoringc  42070  ply1sclrmsm  42171  lincfsuppcl  42202  zofldiv2  42325  elbigolo1  42351  blennn0em1  42385  blennn0e2  42388  dig2nn0ld  42398  nn0sumshdiglem2  42416