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

Theorem anim1i 323
Description: Introduce conjunct to both sides of an implication. (Contributed by NM, 5-Aug-1993.)
Hypothesis
Ref Expression
anim1i.1 (φψ)
Assertion
Ref Expression
anim1i ((φ χ) → (ψ χ))

Proof of Theorem anim1i
StepHypRef Expression
1 anim1i.1 . 2 (φψ)
2 id 19 . 2 (χχ)
31, 2anim12i 321 1 ((φ χ) → (ψ χ))
Colors of variables: wff set class
Syntax hints:  wi 4   wa 97
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101
This theorem is referenced by:  sylanl1  384  sylanr1  386  mpan10  446  sbcof2  1669  sbidm  1709  disamis  1989  fun11uni  4891  fabexg  4998  fores  5036  f1oabexg  5059  fun11iun  5068  fvelrnb  5142  ssimaex  5155  foeqcnvco  5351  f1eqcocnv  5352  isoini  5378  brtposg  5787  elni2  6168  dmaddpqlem  6230  nqpi  6231  ltexnqq  6260  nq0nn  6291  nqnq0a  6303  nqnq0m  6304  elnp1st2nd  6324  mullocprlem  6408  cnegexlem3  6775
  Copyright terms: Public domain W3C validator