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  3981  ralxfr2d  4161  rexxfr2d  4162  nlimsucg  4241  relop  4428  resiexg  4595  iotass  4826  fnbr  4942  f1o00  5102  fnex  5324  acexmidlemab  5446  f1ocnv2d  5643  ofrval  5661  eloprabi  5761  1stconst  5781  2ndconst  5782  poxp  5791  smodm2  5848  smoiso  5855  erth  6079  iinerm  6107  nlt1pig  6318  dfplpq2  6331  ltsonq  6375  archnqq  6393  nqnq0pi  6413  prarloclemn  6474  genprndl  6497  genprndu  6498  genpdisj  6499  addlocprlemgt  6510  addlocpr  6512  addnqpr1lemrl  6529  addnqpr1lemru  6530  ltpopr  6559  ltexprlemloc  6571  ltexprlemrl  6574  cnegex  6938  mullt0  7222  mulge0  7355  divap0  7397  div2negap  7445  prodgt0  7550  ltmul12a  7558  recgt1i  7596  nn0lt2  8047  peano5uzti  8071  eluzp1m1  8221  eluzaddi  8224  eluzsubi  8225  uz2m1nn  8267  rphalflt  8335  ixxdisj  8490  iccgelb  8519  icodisj  8578  iccf1o  8590  fzsuc2  8657  fzonmapblen  8759
  Copyright terms: Public domain W3C validator