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

Theorem biimpa 280
Description: Inference from a logical equivalence. (Contributed by NM, 3-May-1994.)
Hypothesis
Ref Expression
biimpa.1
Assertion
Ref Expression
biimpa

Proof of Theorem biimpa
StepHypRef Expression
1 biimpa.1 . . 3
21biimpd 132 . 2
32imp 115 1
Colors of variables: wff set class
Syntax hints:   wi 4   wa 97   wb 98
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100
This theorem depends on definitions:  df-bi 110
This theorem is referenced by:  simprbda  365  simplbda  366  pm5.1  533  bimsc1  869  biimp3a  1234  equsex  1613  euor  1923  euan  1953  cgsexg  2583  cgsex2g  2584  cgsex4g  2585  ceqsex  2586  sbciegft  2787  sbeqalb  2809  syl5sseq  2987  euotd  3982  ralxfr2d  4162  rexxfr2d  4163  nlimsucg  4242  relop  4429  resiexg  4596  iotass  4827  fnbr  4944  f1o00  5104  fnex  5326  acexmidlemab  5449  f1ocnv2d  5646  ofrval  5664  eloprabi  5764  1stconst  5784  2ndconst  5785  poxp  5794  smodm2  5851  smoiso  5858  erth  6086  iinerm  6114  nlt1pig  6325  dfplpq2  6338  ltsonq  6382  archnqq  6400  nqnq0pi  6421  prarloclemn  6482  genprndl  6504  genprndu  6505  genpdisj  6506  addlocprlemgt  6517  addlocpr  6519  nqprl  6533  addnqprlemrl  6538  addnqprlemru  6539  ltpopr  6569  ltexprlemloc  6581  ltexprlemrl  6584  cauappcvgprlemladdfu  6626  cauappcvgprlemladdfl  6627  caucvgprlemladdfu  6648  cnegex  6986  mullt0  7270  mulge0  7403  divap0  7445  div2negap  7493  prodgt0  7599  ltmul12a  7607  recgt1i  7645  nn0lt2  8098  peano5uzti  8122  eluzp1m1  8272  eluzaddi  8275  eluzsubi  8276  uz2m1nn  8318  rphalflt  8387  ixxdisj  8542  iccgelb  8571  icodisj  8630  iccf1o  8642  fzsuc2  8711  fzonmapblen  8813  expubnd  8965  bernneq  9022  bernneq2  9023  sqrt0rlem  9212
  Copyright terms: Public domain W3C validator