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

Theorem exp44 441
 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 424 . 2 (𝜑 → ((𝜓𝜒) → (𝜃𝜏)))
32expd 419 1 (𝜑 → (𝜓 → (𝜒 → (𝜃𝜏))))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ wa 399 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 210  df-an 400 This theorem is referenced by:  wefrc  5517  tz7.7  6192  oalimcl  8187  unbenlem  16254  rnelfm  22599  uspgr2wlkeqi  27481  1pthon2v  27982  spansncvi  29479  atom1d  30180  chirredlem3  30219  conway  33477  finminlem  33926  cvlcvr1  36786  lhpexle2lem  37456  trlord  38016  cdlemkid4  38381  dihord6apre  38703  dihglbcpreN  38747
 Copyright terms: Public domain W3C validator