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

Theorem exp44 428
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 411 . 2 (𝜑 → ((𝜓𝜒) → (𝜃𝜏)))
32expd 404 1 (𝜑 → (𝜓 → (𝜒 → (𝜃𝜏))))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 384
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 198  df-an 385
This theorem is referenced by:  wefrc  5271  tz7.7  5934  oalimcl  7845  unbenlem  15893  rnelfm  22036  uspgr2wlkeqi  26835  1pthon2v  27389  spansncvi  28902  atom1d  29603  chirredlem3  29642  conway  32286  finminlem  32688  cvlcvr1  35227  lhpexle2lem  35897  trlord  36457  cdlemkid4  36822  dihord6apre  37144  dihglbcpreN  37188
  Copyright terms: Public domain W3C validator