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

Theorem impr 377
 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 114 . 2 (𝜑 → (𝜓 → (𝜒𝜃)))
32imp32 255 1 ((𝜑 ∧ (𝜓𝜒)) → 𝜃)
 Colors of variables: wff set class Syntax hints:   → wi 4   ∧ wa 103 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107 This theorem is referenced by:  reximddv2  2559  moi2  2889  preq12bg  3732  ordsuc  4516  f1ocnv2d  6014  supisoti  6942  caucvgsrlemoffres  7699  prodge0  8704  un0addcl  9102  un0mulcl  9103  peano2uz2  9250  elfz2nn0  9992  fzind2  10116  expaddzap  10441  expmulzap  10443  cau3lem  10991  climuni  11167  climrecvg1n  11222  fisumcom2  11312  fprodcom2fi  11500  dvdsval2  11663  algcvga  11899  lcmgcdlem  11925  divgcdcoprmex  11950  epttop  12429  cncnp  12569  cnconst  12573  bl2in  12742  metcnpi  12854  metcnpi2  12855  metcnpi3  12856
 Copyright terms: Public domain W3C validator