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

Theorem impr 379
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 115 . 2 (𝜑 → (𝜓 → (𝜒𝜃)))
32imp32 257 1 ((𝜑 ∧ (𝜓𝜒)) → 𝜃)
Colors of variables: wff set class
Syntax hints:  wi 4  wa 104
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108
This theorem is referenced by:  reximddv2  2582  moi2  2918  preq12bg  3771  ordsuc  4559  f1ocnv2d  6069  supisoti  7003  caucvgsrlemoffres  7787  prodge0  8797  un0addcl  9195  un0mulcl  9196  peano2uz2  9346  elfz2nn0  10095  fzind2  10222  expaddzap  10547  expmulzap  10549  cau3lem  11104  climuni  11282  climrecvg1n  11337  fisumcom2  11427  fprodcom2fi  11615  dvdsval2  11778  algcvga  12031  lcmgcdlem  12057  divgcdcoprmex  12082  prmpwdvds  12333  isgrpinv  12813  dvdsrcl2  13090  epttop  13254  cncnp  13394  cnconst  13398  bl2in  13567  metcnpi  13679  metcnpi2  13680  metcnpi3  13681
  Copyright terms: Public domain W3C validator