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

Theorem exp44 639
 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 629 . 2 (𝜑 → ((𝜓𝜒) → (𝜃𝜏)))
32expd 451 1 (𝜑 → (𝜓 → (𝜒 → (𝜃𝜏))))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ wa 383 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 196  df-an 385 This theorem is referenced by:  wefrc  5032  tz7.7  5666  oalimcl  7527  unbenlem  15450  rnelfm  21567  wwlknimp  26215  spansncvi  27895  atom1d  28596  chirredlem3  28635  finminlem  31482  cvlcvr1  33644  lhpexle2lem  34313  trlord  34875  cdlemkid4  35240  dihord6apre  35563  dihglbcpreN  35607  uspgr2wlkeqi  40856  1pthon2v-av  41320
 Copyright terms: Public domain W3C validator