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

Theorem biimpa 471
Description: 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
StepHypRef Expression
1 biimpa.1 . . 3  |-  ( ph  ->  ( ps  <->  ch )
)
21biimpd 199 . 2  |-  ( ph  ->  ( ps  ->  ch ) )
32imp 419 1  |-  ( (
ph  /\  ps )  ->  ch )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 177    /\ wa 359
This theorem is referenced by:  simprbda  607  simplbda  608  pm5.1  831  bimsc1  905  biimp3a  1283  equsex  1969  euor  2289  euan  2319  cgsexg  2955  cgsex2g  2956  cgsex4g  2957  ceqsex  2958  sbciegft  3159  sbeqalb  3181  syl5sseq  3364  euotd  4425  ralxfr2d  4706  elpwunsn  4724  limsssuc  4797  relop  4990  resiexg  5155  fnbr  5514  f1o00  5677  dffv2  5763  iinpreima  5827  funressn  5886  fnex  5928  weniso  6042  f1ocnv2d  6262  ofrval  6282  eloprabi  6380  1stconst  6402  2ndconst  6403  frxp  6423  poxp  6425  riotasvdOLD  6560  smodm2  6584  smoiso  6591  tz7.44lem1  6630  oev2  6734  oesuclem  6736  oecl  6748  omordi  6776  omwordri  6782  omword2  6784  omordlim  6787  omlimcl  6788  omeulem2  6793  oeordi  6797  oewordri  6802  oelim2  6805  oeoa  6807  oeoe  6809  nnawordi  6831  nnaordex  6848  erth  6916  iiner  6943  pw2f1olem  7179  pw2f1o  7180  onomeneq  7263  onfin2  7265  unxpdomlem2  7281  isinf  7289  findcard2  7315  fipreima  7378  fipwss  7400  cantnfp1lem3  7600  carden2b  7818  carddomi2  7821  infxpenlem  7859  acni2  7891  numacn  7894  alephfp  7953  pwsdompw  8048  ackbij2lem3  8085  cfeq0  8100  cfsuc  8101  cfsmolem  8114  domfin4  8155  axdc3lem2  8295  axdc3lem4  8297  alephreg  8421  fpwwe2  8482  winainflem  8532  r1limwun  8575  inar1  8614  grudomon  8656  nlt1pi  8747  indpi  8748  nqereu  8770  ltbtwnnq  8819  prlem934  8874  prlem936  8888  addgt0sr  8943  leltne  9128  ne0gt0  9142  mullt0  9511  msqgt0  9512  mulne0  9628  divne0  9654  div2neg  9701  ltmul12a  9830  recgt1i  9871  nn2ge  9989  peano5uzi  10322  eluzp1m1  10473  eluzaddi  10476  eluzsubi  10477  uz2m1nn  10514  rpnnen1lem5  10568  rphalflt  10602  xrleltne  10702  max0sub  10746  xmulpnf1n  10821  xmulge0  10827  xadddi  10838  supxr  10855  supxr2  10856  ixxdisj  10895  ixxun  10896  ixxub  10901  ixxlb  10902  icodisj  10986  difreicc  10992  iccf1o  11003  fzsuc2  11068  elfznelfzo  11155  flge0nn0  11188  flge1nn  11189  seqf1olem2  11326  expubnd  11403  sqlecan  11450  bernneq  11468  bernneq2  11469  expnbnd  11471  discr1  11478  facwordi  11543  faclbnd4lem4  11550  bcpasc  11575  elprchashprn2  11630  iswrdi  11694  ccatass  11713  revccat  11761  revrev  11762  revco  11766  s2f1o  11826  s4f1o  11828  sqr0lem  12009  sqrlem2  12012  sqrlem7  12017  max0add  12078  recval  12089  nnabscl  12092  absmax  12096  sqreulem  12126  climi0  12269  lo1bdd2  12281  rlimresb  12322  lo1eq  12325  rlimeq  12326  isercolllem3  12423  climsup  12426  fsumsplit  12496  fsumcom2  12521  explecnv  12607  eftlub  12673  sin02gt0  12756  rpnnen2lem10  12786  odd2np1  12871  oexpneg  12874  bitsf1  12921  sadcaddlem  12932  bitsuz  12949  rplpwr  13019  rppwr  13020  nn0seqcvgd  13024  qredeq  13069  qgt0numnn  13106  phibndlem  13122  coprimeprodsq2  13147  pythagtrip  13171  fldivp1  13229  unbenlem  13239  4sqlem9  13277  4sqlem15  13290  4sqlem16  13291  vdwlem6  13317  vdwlem10  13321  vdwlem11  13322  vdwlem13  13324  vdw  13325  mreuni  13788  cidpropd  13899  subsubc  14013  ffthiso  14089  fuciso  14135  setcmon  14205  setcepi  14206  catciso  14225  hofcl  14319  hofpropd  14327  yonedalem4c  14337  yonedainv  14341  imasmnd  14696  pwsco1mhm  14732  imasgrp  14897  subginv  14914  subgmulg  14921  eqger  14953  subgga  15040  orbstafun  15051  orbsta  15053  symggrp  15066  dfod2  15163  gexval  15175  gex1  15188  sylow2blem1  15217  sylow3lem1  15224  pj1eu  15291  efgredlema  15335  frgp0  15355  frgpmhm  15360  odadd1  15426  0cyg  15465  gsumzres  15480  gsumzsplit  15492  dprd2dlem1  15562  dprd2da  15563  dmdprdsplit2  15567  dprdsplit  15569  pgpfaclem3  15604  ablfac2  15610  imasrng  15688  subrg1  15841  abvneg  15885  lmhmf1o  16085  lmhmima  16086  reslmhm2b  16093  lsmspsn  16119  lspdisj  16160  lidlmcl  16251  fidomndrnglem  16329  mplsubglem  16461  mplmonmul  16490  mplbas2  16494  subrgascl  16521  subrgasclcl  16522  absabv  16719  elcls  17100  clsndisj  17102  isclo2  17115  neiuni  17149  neissex  17154  neiptopreu  17160  tgrest  17185  neitr  17206  tgcnp  17279  lmfpm  17321  lmcl  17323  lmss  17324  lmff  17327  ist1-2  17373  cnt1  17376  cmpsublem  17424  clscon  17454  kgeni  17530  kgenidm  17540  txcnpi  17601  ptpjopn  17605  ptclsg  17608  txcmplem1  17634  qtoptop2  17692  qtoptopon  17697  r0sep  17741  ptunhmeo  17801  t0kq  17811  fsubbas  17860  neifil  17873  uffixsn  17918  ufildr  17924  rnelfm  17946  isfcls2  18006  uffclsflim  18024  alexsublem  18036  cnextfun  18056  cnextfvval  18057  cnextf  18058  cnextcn  18059  tmdcn2  18080  symgtgp  18092  tsmssplit  18142  ustuni  18217  trust  18220  utoptop  18225  restutop  18228  restutopopn  18229  ustuqtop1  18232  ustuqtop2  18233  ustuqtop3  18234  ustuqtop4  18235  utop2nei  18241  utop3cls  18242  isucn2  18270  ucncn  18276  trcfilu  18285  cfiluweak  18286  psmetdmdm  18297  xblss2ps  18392  xmeter  18424  prdsbl  18482  neibl  18492  methaus  18511  prdsxmslem2  18520  metusttoOLD  18548  metustto  18549  metustexhalfOLD  18554  metustexhalf  18555  metustOLD  18558  metust  18559  cfilucfilOLD  18560  cfilucfil  18561  metutopOLD  18573  psmetutop  18574  metucnOLD  18579  metucn  18580  tngngp2  18654  tngngp  18656  tgqioo  18792  xrsxmet  18801  icccmplem1  18814  icccmplem2  18815  cnmpt2pc  18914  iihalf2  18919  icoopnst  18925  iocopnst  18926  xrhmeo  18932  lebnumlem1  18947  lebnumlem3  18949  pi1blem  19025  pi1grplem  19035  pi1xfrf  19039  pi1xfr  19041  pi1xfrcnvlem  19042  pi1cof  19045  pi1coghm  19047  cmetcaulem  19202  causs  19212  metcld  19219  lmcau  19226  cmetcusp  19269  minveclem4  19294  ivthlem2  19310  ivthlem3  19311  ivthicc  19316  ovolshftlem1  19366  ovolicc1  19373  ovolicopnf  19381  volfiniun  19402  uniioombllem3  19438  dyaddisjlem  19448  vitalilem2  19462  itg1ge0  19539  mbfi1fseqlem3  19570  xrge0f  19584  itg2seq  19595  itg2monolem1  19603  itg2addlem  19611  itg2gt0  19613  iblcnlem  19641  itgss3  19667  itgsplit  19688  dvnff  19770  dvferm2  19832  dvlip2  19840  dveq0  19845  dvge0  19851  dvcnvre  19864  dvfsumle  19866  dvfsumabs  19868  dvfsumlem2  19872  ftc1lem2  19881  ftc1lem4  19884  ftc1lem5  19885  ftc1cn  19888  ftc2  19889  itgsubstlem  19893  evlsval2  19902  mpfind  19926  coe1mul3  19983  ply1divex  20020  dgrlem  20109  dgrlb  20116  coemulhi  20133  dgrlt  20145  dgrmul  20149  plydivlem4  20174  fta1  20186  aaliou2b  20219  taylplem2  20241  dvtaylp  20247  ulmcau  20272  tanabsge  20375  sinq12gt0  20376  argimgt0  20468  cxplea  20548  cxple2  20549  cxpsqr  20555  cxpaddlelem  20596  loglesqr  20603  ang180lem2  20613  lawcos  20619  logrec  20622  asinlem3a  20671  asinlem3  20672  asinsin  20693  atanlogaddlem  20714  atanlogadd  20715  atanlogsub  20717  atantan  20724  atanbnd  20727  atantayl2  20739  efrlim  20769  wilthlem2  20813  basellem2  20825  sqfpc  20881  ppieq0  20920  sqff1o  20926  fsumdvdscom  20931  ppiub  20949  chpeq0  20953  chtleppi  20955  fsumvma  20958  fsumvma2  20959  mersenne  20972  dchrabs2  21007  dchr1re  21008  dchrpt  21012  lgsdilem  21067  lgsdinn0  21085  lgsquad3  21106  m1lgs  21107  2sqlem6  21114  rpvmasumlem  21142  dchrisumlem3  21146  dchrisum0flblem1  21163  pntibndlem2a  21245  pntlem3  21264  padicabv  21285  usgra1  21354  usgraedg4  21367  nbgraop  21397  nbgracnvfv  21411  nbcusgra  21433  wlkdvspthlem  21568  fargshiftf1  21585  fargshiftfo  21586  eupatrl  21651  eupap1  21659  vcoprnelem  22018  cnnv  22129  nmounbseqi  22239  nmounbseqiOLD  22240  nmlnogt0  22259  nmblolbii  22261  blocnilem  22266  ajmoi  22321  minvecolem4  22343  hhnv  22628  norm1  22712  hhssnv  22725  pjhtheu  22857  pjpreeq  22861  spanunsni  23042  fh1  23081  fh2  23082  cm2j  23083  chscllem4  23103  pjid  23158  adjmo  23296  eleigveccl  23423  eigvalcl  23425  eigvec1  23426  eighmre  23427  eighmorth  23428  nmop0h  23455  nmbdoplbi  23488  nmcoplbi  23492  nmophmi  23495  lncnopbd  23501  nmbdfnlbi  23513  nmcfnlbi  23516  cnlnadjeui  23541  branmfn  23569  rnbra  23571  nmopleid  23603  strlem5  23719  hstrlem5  23727  dmdbr3  23769  dmdbr4  23770  mdsl3  23780  hatomistici  23826  cvexchlem  23832  chirredlem1  23854  chirredlem2  23855  chirredi  23858  atcvat3i  23860  atcvat4i  23861  atabsi  23865  mdsymlem1  23867  mdsymlem3  23869  mdsymlem5  23871  dmdbr5ati  23886  cdj1i  23897  elabreximd  23952  elpreq  23960  f1o3d  24002  disjdsct  24051  xrofsup  24087  iccgelb  24097  eliccelico  24101  elicoelioo  24102  numdenneg  24121  xrge0addgt0  24175  xrge0adddir  24176  xrge0npcan  24177  kerf1hrm  24223  metideq  24249  unitdivcld  24260  cnre2csqlem  24269  fmcncfil  24278  lmxrge0  24298  zrhunitpreima  24323  elzdif0  24325  qqhval2lem  24326  qqhf  24331  indf1ofs  24384  esumfsup  24421  esumpcvgval  24429  sigasspw  24460  issgon  24467  meascnbl  24534  voliune  24546  volfiniune  24547  ballotlemfrcn0  24748  ballotlemirc  24750  subfacp1lem5  24831  subfacp1lem6  24832  erdszelem9  24846  ptpcon  24881  rescon  24894  cvmlift3lem7  24973  fprodser  25236  fprodsplit  25250  fprodcom2  25269  sspred  25396  trpredrec  25463  axcontlem2  25816  axcontlem12  25826  btwnintr  25865  btwnouttr  25870  cgrxfr  25901  btwnconn1lem12  25944  colinbtwnle  25964  lineelsb2  25994  onintopsscon  26102  mblfinlem  26151  itg2gt0cn  26167  itgaddnclem2  26171  ftc1cnnclem  26185  ftc1cnnc  26186  areacirclem6  26194  areacirc  26195  nn0prpwlem  26223  locfindis  26283  neibastop3  26289  fdc  26347  incsequz  26350  blbnd  26394  prdstotbnd  26401  cnpwstotbnd  26404  ismtyres  26415  rngohomf  26480  rngohom1  26482  rngohomadd  26483  rngohommul  26484  idlss  26524  idl0cl  26526  idladdcl  26527  idllmulcl  26528  idlrmulcl  26529  maxidlnr  26550  maxidlmax  26551  smprngopr  26560  pridlc  26579  ceqsex3OLD  26607  mzpindd  26701  lzunuz  26724  2rexfrabdioph  26754  irrapxlem3  26785  pellexlem2  26791  pellexlem5  26794  pell1234qrreccl  26815  pell14qrdich  26830  pell1qrge1  26831  elpell1qr2  26833  reglogltb  26852  reglogleb  26853  rmxycomplete  26878  2nn0ind  26906  congabseq  26937  acongrep  26943  acongeq  26946  dvdsleabs2  26953  jm2.22  26964  jm2.26lem3  26970  pw2f1ocnv  27006  limsuc2  27013  fnwe2lem3  27025  aomclem6  27032  kercvrlsm  27057  pwssplit0  27063  pwssplit1  27064  pwssplit4  27067  frlmbas  27099  elfilspd  27131  f1lindf  27168  lpirlnr  27197  hashgcdeq  27393  dvconstbi  27427  mulltgt0  27568  refsumcn  27576  cncmpmax  27578  climinf  27607  climreeq  27614  stoweidlem27  27651  stoweidlem29  27653  stoweidlem31  27655  stoweidlem34  27658  stoweidlem48  27672  stoweidlem59  27683  sigarcol  27729  reuan  27833  ndmaovg  27923  iswrd0i  28007  swrd0swrd  28017  swrdswrdlem  28018  swrdswrd  28019  swrdswrd0  28021  swrdccat3a0  28023  swrdccatin2  28026  swrdccat3b  28039  usgra2pthlem1  28048  usg2spthonot  28093  frgrancvvdeqlemA  28148  frgrancvvdeqlemB  28149  frgrancvvdeqlemC  28150  frgrawopreglem4  28158  bi2imp  28287  a9e2ndeqALT  28762  bnj563  28829  bnj1001  29047  lshpnel2N  29480  islsati  29489  lkr0f  29589  lfl1dim  29616  lfl1dim2N  29617  omlfh1N  29753  leat  29788  atlatmstc  29814  cvlatexch3  29833  lnnat  29921  cvrat3  29936  cvrat4  29937  3dim3  29963  dalem4  30159  dalem39  30205  paddasslem12  30325  psubcliN  30432  pmapojoinN  30462  lhpm0atN  30523  lhprelat3N  30534  trlnid  30673  trlval3  30681  cdleme22b  30835  trljco  31234  diaglbN  31550  dibvalrel  31658  dicvalrelN  31680  diclspsn  31689  dih1dimatlem  31824  dihlatat  31832  lcfl6  31995  lcfl8  31997  lcfrvalsnN  32036  lcfrlem9  32045  mapdheq2  32224  hlhillcs  32456  hlhilhillem  32458
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