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

Theorem exp44 638
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 628 . 2 (𝜑 → ((𝜓𝜒) → (𝜃𝜏)))
32expd 450 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 195  df-an 384
This theorem is referenced by:  wefrc  5021  tz7.7  5651  oalimcl  7504  unbenlem  15398  rnelfm  21514  wwlknimp  26008  spansncvi  27688  atom1d  28389  chirredlem3  28428  finminlem  31275  cvlcvr1  33427  lhpexle2lem  34096  trlord  34658  cdlemkid4  35023  dihord6apre  35346  dihglbcpreN  35390  uspgr2wlkeqi  40837  1pthon2v-av  41301
  Copyright terms: Public domain W3C validator