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

Theorem expr 357
Description: Export a wff from a right conjunct. (Contributed by Jeff Hankins, 30-Aug-2009.)
Hypothesis
Ref Expression
expr.1 ((φ (ψ χ)) → θ)
Assertion
Ref Expression
expr ((φ ψ) → (χθ))

Proof of Theorem expr
StepHypRef Expression
1 expr.1 . . 3 ((φ (ψ χ)) → θ)
21exp32 347 . 2 (φ → (ψ → (χθ)))
32imp 115 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:  rexlimdvaa  2428  issod  4047  ordsuc  4241  fcof1  5366  riota5f  5435  ovmpt2df  5574  tfrlemi1  5887  addnq0mo  6430  mulnq0mo  6431  genprndl  6504  genprndu  6505  addlocpr  6519  ltexprlemm  6574  ltexprlemopl  6575  ltexprlemopu  6577  ltexprlemfl  6583  ltexprlemfu  6585  aptiprleml  6611  addsrmo  6671  mulsrmo  6672  prodge0  7601  un0addcl  7991  un0mulcl  7992  iseqfveq2  8905  expnegzap  8943
  Copyright terms: Public domain W3C validator