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

Theorem imp32 257
Description: An importation inference. (Contributed by NM, 26-Apr-1994.)
Hypothesis
Ref Expression
imp3.1 (𝜑 → (𝜓 → (𝜒𝜃)))
Assertion
Ref Expression
imp32 ((𝜑 ∧ (𝜓𝜒)) → 𝜃)

Proof of Theorem imp32
StepHypRef Expression
1 imp3.1 . . 3 (𝜑 → (𝜓 → (𝜒𝜃)))
21impd 254 . 2 (𝜑 → ((𝜓𝜒) → 𝜃))
32imp 124 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
This theorem is referenced by:  imp42  354  impr  379  anasss  399  an13s  567  3expb  1206  reuss2  3430  reupick  3434  po2nr  4327  fvmptt  5628  fliftfund  5819  f1ocnv2d  6098  addclpi  7356  addnidpig  7365  mulnqprl  7597  mulnqpru  7598  ltsubrp  9720  ltaddrp  9721  divgcdcoprm0  12133  infpnlem1  12391  imasgrp2  13052  imasrng  13310  imasring  13414  innei  14123  tgcnp  14169  isxmetd  14307
  Copyright terms: Public domain W3C validator