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

Theorem exp44 424
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 407 . 2 (𝜑 → ((𝜓𝜒) → (𝜃𝜏)))
32expd 400 1 (𝜑 → (𝜓 → (𝜒 → (𝜃𝜏))))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 382
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 197  df-an 383
This theorem is referenced by:  wefrc  5243  tz7.7  5890  oalimcl  7794  unbenlem  15815  rnelfm  21973  uspgr2wlkeqi  26775  1pthon2v  27329  spansncvi  28847  atom1d  29548  chirredlem3  29587  conway  32243  finminlem  32645  cvlcvr1  35144  lhpexle2lem  35814  trlord  36375  cdlemkid4  36740  dihord6apre  37063  dihglbcpreN  37107
  Copyright terms: Public domain W3C validator