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

Theorem exp4c 635
 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 197  df-an 385 This theorem is referenced by:  exp5j  644  oawordri  7675  oaordex  7683  odi  7704  pssnn  8219  alephval3  8971  dfac2  8991  axdc4lem  9315  leexp1a  12959  wrdsymb0  13371  swrdnd2  13479  coprmproddvds  15424  lmodvsmmulgdi  18946  assamulgscm  19398  2ndcctbss  21306  2pthnloop  26683  wwlksnext  26856  frgrregord013  27382  atcvatlem  29372  exp5g  32422  cdleme48gfv1  36141  cdlemg6e  36227  dihord5apre  36868  dihglblem5apreN  36897  iccpartgt  41688  lmodvsmdi  42488  lindslinindsimp1  42571  nn0sumshdiglemB  42739
 Copyright terms: Public domain W3C validator