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

Theorem exp4c 634
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 451 . 2 (𝜑 → ((𝜓𝜒) → (𝜃𝜏)))
32expd 451 1 (𝜑 → (𝜓 → (𝜒 → (𝜃𝜏))))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 383
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 196  df-an 385
This theorem is referenced by:  exp5j  643  oawordri  7495  oaordex  7503  odi  7524  pssnn  8041  alephval3  8794  dfac2  8814  axdc4lem  9138  leexp1a  12739  wrdsymb0  13143  swrdnd2  13234  coprmproddvds  15164  lmodvsmmulgdi  18670  assamulgscm  19120  2ndcctbss  21016  wwlknext  26046  frgraregord013  26439  atcvatlem  28422  exp5g  31261  cdleme48gfv1  34636  cdlemg6e  34722  dihord5apre  35363  dihglblem5apreN  35392  iccpartgt  39760  2pthnloop  40929  wwlksnext  41091  av-frgraregord013  41541  lmodvsmdi  41949  lindslinindsimp1  42032  nn0sumshdiglemB  42204
  Copyright terms: Public domain W3C validator