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

Theorem exp4c 423
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 404 . 2 (𝜑 → ((𝜓𝜒) → (𝜃𝜏)))
32expd 404 1 (𝜑 → (𝜓 → (𝜒 → (𝜃𝜏))))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 384
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 198  df-an 385
This theorem is referenced by:  exp5j  436  oawordri  7837  oaordex  7845  odi  7866  pssnn  8387  alephval3  9186  dfac2b  9206  dfac2OLD  9208  axdc4lem  9532  leexp1a  13129  wrdsymb0  13523  swrdnd2  13638  coprmproddvds  15660  lmodvsmmulgdi  19170  assamulgscm  19627  2ndcctbss  21541  2pthnloop  26922  wwlksnext  27099  frgrregord013  27714  atcvatlem  29703  exp5g  32744  cdleme48gfv1  36495  cdlemg6e  36581  dihord5apre  37221  dihglblem5apreN  37250  iccpartgt  42100  lmodvsmdi  42835  lindslinindsimp1  42918  nn0sumshdiglemB  43086
  Copyright terms: Public domain W3C validator