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

Theorem imp32 255
 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 252 . 2 (𝜑 → ((𝜓𝜒) → 𝜃))
32imp 123 1 ((𝜑 ∧ (𝜓𝜒)) → 𝜃)
 Colors of variables: wff set class Syntax hints:   → wi 4   ∧ wa 103 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106 This theorem is referenced by:  imp42  351  impr  376  anasss  396  an13s  556  3expb  1182  reuss2  3356  reupick  3360  po2nr  4231  fvmptt  5512  fliftfund  5698  f1ocnv2d  5974  addclpi  7142  addnidpig  7151  mulnqprl  7383  mulnqpru  7384  ltsubrp  9485  ltaddrp  9486  divgcdcoprm0  11789  innei  12342  tgcnp  12388  isxmetd  12526
 Copyright terms: Public domain W3C validator