ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  biimpa Unicode version

Theorem biimpa 284
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 136 . 2  |-  ( ph  ->  ( ps  ->  ch ) )
32imp 119 1  |-  ( (
ph  /\  ps )  ->  ch )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 101    <-> wb 102
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 103  ax-ia2 104
This theorem depends on definitions:  df-bi 114
This theorem is referenced by:  simprbda  369  simplbda  370  pm5.1  543  bimsc1  881  biimp3a  1251  equsex  1632  euor  1942  euan  1972  cgsexg  2606  cgsex2g  2607  cgsex4g  2608  ceqsex  2609  sbciegft  2816  sbeqalb  2842  syl5sseq  3021  euotd  4019  ralxfr2d  4224  rexxfr2d  4225  nlimsucg  4318  wetriext  4329  relop  4514  resiexg  4681  iotass  4912  fnbr  5029  f1o00  5189  fnex  5411  acexmidlemab  5534  f1ocnv2d  5732  ofrval  5750  eloprabi  5850  1stconst  5870  2ndconst  5871  poxp  5881  smodm2  5941  smoiso  5948  erth  6181  iinerm  6209  phplem4dom  6355  findcard2  6377  findcard2s  6378  nlt1pig  6497  dfplpq2  6510  ltsonq  6554  archnqq  6573  nqnq0pi  6594  prarloclemn  6655  genprndl  6677  genprndu  6678  genpdisj  6679  addlocprlemgt  6690  addlocpr  6692  nqprl  6707  nqpru  6708  addnqprlemrl  6713  addnqprlemru  6714  mulnqprlemrl  6729  mulnqprlemru  6730  ltpopr  6751  ltexprlemloc  6763  ltexprlemrl  6766  cauappcvgprlemladdfu  6810  cauappcvgprlemladdfl  6811  caucvgprlemladdfu  6833  axcaucvglemres  7031  cnegex  7252  mullt0  7549  mulge0  7684  divap0  7737  div2negap  7786  prodgt0  7893  ltmul12a  7901  recgt1i  7939  div4p1lem1div2  8235  nn0lt2  8380  peano5uzti  8405  eluzp1m1  8592  eluzaddi  8595  eluzsubi  8596  uz2m1nn  8639  rphalflt  8710  ixxdisj  8873  iccgelb  8902  icodisj  8961  iccf1o  8973  fzsuc2  9043  fzonmapblen  9145  flqge0nn0  9243  flqge1nn  9244  modfzo0difsn  9345  expubnd  9477  bernneq  9537  bernneq2  9538  nn0opthlem2d  9589  facwordi  9608  bcpasc  9634  recvguniq  9822  sqrt0rlem  9830  resqrexlemover  9837  resqrexlemcalc3  9843  resqrexlemgt0  9847  resqrexlemoverl  9848  recvalap  9924  nnabscl  9927  climi0  10041  climge0  10076  dvdslelemd  10155  dvdsleabs2  10158  mulmoddvds  10175  odd2np1  10184  oexpneg  10188  mod2eq1n2dvds  10191  sqoddm1div8z  10198  oddpwdclemdvds  10258  oddpwdclemndvds  10259  oddpwdclemodd  10260  nn0seqcvgd  10263
  Copyright terms: Public domain W3C validator