MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  exp44 Structured version   Visualization version   GIF version

Theorem exp44 436
Description: An exportation inference. (Contributed by NM, 26-Apr-1994.)
Hypothesis
Ref Expression
exp44.1 ((𝜑 ∧ ((𝜓𝜒) ∧ 𝜃)) → 𝜏)
Assertion
Ref Expression
exp44 (𝜑 → (𝜓 → (𝜒 → (𝜃𝜏))))

Proof of Theorem exp44
StepHypRef Expression
1 exp44.1 . . 3 ((𝜑 ∧ ((𝜓𝜒) ∧ 𝜃)) → 𝜏)
21exp32 419 . 2 (𝜑 → ((𝜓𝜒) → (𝜃𝜏)))
32expd 414 1 (𝜑 → (𝜓 → (𝜒 → (𝜃𝜏))))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 394
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This theorem depends on definitions:  df-bi 206  df-an 395
This theorem is referenced by:  wefrc  5672  tz7.7  6397  oalimcl  8581  unbenlem  16880  rnelfm  23901  conway  27778  uspgr2wlkeqi  29534  1pthon2v  30035  spansncvi  31534  atom1d  32235  chirredlem3  32274  finminlem  35933  cvlcvr1  38941  lhpexle2lem  39612  trlord  40172  cdlemkid4  40537  dihord6apre  40859  dihglbcpreN  40903
  Copyright terms: Public domain W3C validator