Intuitionistic Logic Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  ILE Home  >  Th. List  >  expr 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  2434  issod  4056  ordsuc  4287  fcof1  5423  riota5f  5492  ovmpt2df  5632  tfrlemi1  5946  ordiso2  6357  addnq0mo  6545  mulnq0mo  6546  genprndl  6619  genprndu  6620  addlocpr  6634  ltexprlemm  6698  ltexprlemopl  6699  ltexprlemopu  6701  ltexprlemfl  6707  ltexprlemfu  6709  aptiprleml  6737  caucvgprprlemexbt  6804  addsrmo  6828  mulsrmo  6829  prodge0  7820  un0addcl  8215  un0mulcl  8216  iseqfveq2  9228  iseqshft2  9232  monoord  9235  iseqsplit  9238  expnegzap  9289  caucvgrelemcau  9579  cau3lem  9710
 Copyright terms: Public domain W3C validator