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

Theorem impr 365
 Description: Import a wff into a right conjunct. (Contributed by Jeff Hankins, 30-Aug-2009.)
Hypothesis
Ref Expression
impr.1 ((𝜑𝜓) → (𝜒𝜃))
Assertion
Ref Expression
impr ((𝜑 ∧ (𝜓𝜒)) → 𝜃)

Proof of Theorem impr
StepHypRef Expression
1 impr.1 . . 3 ((𝜑𝜓) → (𝜒𝜃))
21ex 112 . 2 (𝜑 → (𝜓 → (𝜒𝜃)))
32imp32 248 1 ((𝜑 ∧ (𝜓𝜒)) → 𝜃)
 Colors of variables: wff set class Syntax hints:   → wi 4   ∧ wa 101 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 103  ax-ia2 104  ax-ia3 105 This theorem is referenced by:  moi2  2745  preq12bg  3572  ordsuc  4315  f1ocnv2d  5732  supisoti  6414  caucvgsrlemoffres  6942  prodge0  7895  un0addcl  8272  un0mulcl  8273  peano2uz2  8404  elfz2nn0  9075  fzind2  9197  expaddzap  9464  expmulzap  9466  cau3lem  9941  climuni  10045  climrecvg1n  10098  dvdsval2  10111  ialgcvga  10273
 Copyright terms: Public domain W3C validator