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  7517  oaordex  7525  odi  7546  pssnn  8063  alephval3  8816  dfac2  8836  axdc4lem  9160  leexp1a  12781  wrdsymb0  13194  swrdnd2  13285  coprmproddvds  15215  lmodvsmmulgdi  18721  assamulgscm  19171  2ndcctbss  21068  wwlknext  26252  frgraregord013  26645  atcvatlem  28628  exp5g  31467  cdleme48gfv1  34842  cdlemg6e  34928  dihord5apre  35569  dihglblem5apreN  35598  iccpartgt  39965  2pthnloop  40937  wwlksnext  41099  av-frgraregord013  41549  lmodvsmdi  41957  lindslinindsimp1  42040  nn0sumshdiglemB  42212
 Copyright terms: Public domain W3C validator