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

Theorem exp4c 433
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 416 . 2 (𝜑 → ((𝜓𝜒) → (𝜃𝜏)))
32expd 416 1 (𝜑 → (𝜓 → (𝜒 → (𝜃𝜏))))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 396
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 397
This theorem is referenced by:  exp5j  446  oawordri  8552  oaordex  8560  odi  8581  pssnn  9170  pssnnOLD  9267  alephval3  10107  dfac2b  10127  axdc4lem  10452  leexp1a  14144  wrdsymb0  14503  coprmproddvds  16604  lmodvsmmulgdi  20651  assamulgscm  21674  2ndcctbss  23179  2pthnloop  29243  wwlksnext  29402  frgrregord013  29903  atcvatlem  31893  umgr2cycllem  34417  exp5g  35491  cdleme48gfv1  39710  cdlemg6e  39796  dihord5apre  40436  dihglblem5apreN  40465  iccpartgt  46394  lmodvsmdi  47147  nn0sumshdiglemB  47394
  Copyright terms: Public domain W3C validator