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

Theorem exp4c 431
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 414 . 2 (𝜑 → ((𝜓𝜒) → (𝜃𝜏)))
32expd 414 1 (𝜑 → (𝜓 → (𝜒 → (𝜃𝜏))))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 394
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 206  df-an 395
This theorem is referenced by:  exp5j  444  oawordri  8572  oaordex  8580  odi  8601  pssnn  9198  pssnnOLD  9292  alephval3  10146  dfac2b  10166  axdc4lem  10489  leexp1a  14188  wrdsymb0  14552  coprmproddvds  16659  lmodvsmmulgdi  20869  assamulgscm  21894  2ndcctbss  23447  2pthnloop  29665  wwlksnext  29824  frgrregord013  30325  atcvatlem  32315  umgr2cycllem  34981  exp5g  36028  cdleme48gfv1  40248  cdlemg6e  40334  dihord5apre  40974  dihglblem5apreN  41003  iccpartgt  47035  lmodvsmdi  47797  nn0sumshdiglemB  48044
  Copyright terms: Public domain W3C validator