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

Theorem exp44 437
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 420 . 2 (𝜑 → ((𝜓𝜒) → (𝜃𝜏)))
32expd 415 1 (𝜑 → (𝜓 → (𝜒 → (𝜃𝜏))))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 395
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 207  df-an 396
This theorem is referenced by:  wefrc  5679  tz7.7  6410  oalimcl  8598  unbenlem  16946  rnelfm  23961  conway  27844  uspgr2wlkeqi  29666  1pthon2v  30172  spansncvi  31671  atom1d  32372  chirredlem3  32411  finminlem  36319  cvlcvr1  39340  lhpexle2lem  40011  trlord  40571  cdlemkid4  40936  dihord6apre  41258  dihglbcpreN  41302
  Copyright terms: Public domain W3C validator