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

Theorem exp4c 419
Description: An exportation inference. (Contributed by NM, 26-Apr-1994.)
Hypothesis
Ref Expression
exp4c.1 (𝜑 → (((𝜓𝜒) ∧ 𝜃) → 𝜏))
Assertion
Ref Expression
exp4c (𝜑 → (𝜓 → (𝜒 → (𝜃𝜏))))

Proof of Theorem exp4c
StepHypRef Expression
1 exp4c.1 . . 3 (𝜑 → (((𝜓𝜒) ∧ 𝜃) → 𝜏))
21expd 400 . 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:  exp5j  432  oawordri  7788  oaordex  7796  odi  7817  pssnn  8338  alephval3  9137  dfac2b  9157  dfac2OLD  9159  axdc4lem  9483  leexp1a  13126  wrdsymb0  13535  swrdnd2  13642  coprmproddvds  15584  lmodvsmmulgdi  19108  assamulgscm  19565  2ndcctbss  21479  2pthnloop  26862  wwlksnext  27037  frgrregord013  27594  atcvatlem  29584  exp5g  32634  cdleme48gfv1  36344  cdlemg6e  36430  dihord5apre  37070  dihglblem5apreN  37099  iccpartgt  41886  lmodvsmdi  42686  lindslinindsimp1  42769  nn0sumshdiglemB  42937
  Copyright terms: Public domain W3C validator