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

Theorem exp44 438
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 421 . 2 (𝜑 → ((𝜓𝜒) → (𝜃𝜏)))
32expd 416 1 (𝜑 → (𝜓 → (𝜒 → (𝜃𝜏))))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 396
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 208  df-an 397
This theorem is referenced by:  wefrc  5542  tz7.7  6210  oalimcl  8175  unbenlem  16232  rnelfm  22489  uspgr2wlkeqi  27356  1pthon2v  27859  spansncvi  29356  atom1d  30057  chirredlem3  30096  conway  33161  finminlem  33563  cvlcvr1  36355  lhpexle2lem  37025  trlord  37585  cdlemkid4  37950  dihord6apre  38272  dihglbcpreN  38316
  Copyright terms: Public domain W3C validator