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

Theorem impr 372
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 254 1 ((𝜑 ∧ (𝜓𝜒)) → 𝜃)
Colors of variables: wff set class
Syntax hints:  wi 4  wa 103
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107
This theorem is referenced by:  reximddv2  2478  moi2  2797  preq12bg  3623  ordsuc  4392  f1ocnv2d  5862  supisoti  6759  caucvgsrlemoffres  7406  prodge0  8376  un0addcl  8767  un0mulcl  8768  peano2uz2  8914  elfz2nn0  9587  fzind2  9711  expaddzap  10060  expmulzap  10062  cau3lem  10608  climuni  10742  climrecvg1n  10798  fisumcom2  10893  dvdsval2  11138  algcvga  11372  lcmgcdlem  11398  divgcdcoprmex  11423  epttop  11851
  Copyright terms: Public domain W3C validator