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  5682  tz7.7  6411  oalimcl  8596  unbenlem  16941  rnelfm  23976  conway  27858  uspgr2wlkeqi  29680  1pthon2v  30181  spansncvi  31680  atom1d  32381  chirredlem3  32420  finminlem  36300  cvlcvr1  39320  lhpexle2lem  39991  trlord  40551  cdlemkid4  40916  dihord6apre  41238  dihglbcpreN  41282
  Copyright terms: Public domain W3C validator