ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  biimpa Structured version   GIF 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  6420  prarloclemn  6481  genprndl  6503  genprndu  6504  genpdisj  6505  addlocprlemgt  6516  addlocpr  6518  nqprl  6532  addnqprlemrl  6537  addnqprlemru  6538  ltpopr  6568  ltexprlemloc  6580  ltexprlemrl  6583  cauappcvgprlemladdfu  6625  cauappcvgprlemladdfl  6626  cnegex  6966  mullt0  7250  mulge0  7383  divap0  7425  div2negap  7473  prodgt0  7579  ltmul12a  7587  recgt1i  7625  nn0lt2  8078  peano5uzti  8102  eluzp1m1  8252  eluzaddi  8255  eluzsubi  8256  uz2m1nn  8298  rphalflt  8367  ixxdisj  8522  iccgelb  8551  icodisj  8610  iccf1o  8622  fzsuc2  8691  fzonmapblen  8793  expubnd  8945  bernneq  9002  bernneq2  9003  sqrt0rlem  9192
  Copyright terms: Public domain W3C validator