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

Theorem exp4c 432
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 415 . 2 (𝜑 → ((𝜓𝜒) → (𝜃𝜏)))
32expd 415 1 (𝜑 → (𝜓 → (𝜒 → (𝜃𝜏))))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 395
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 207  df-an 396
This theorem is referenced by:  exp5j  445  oawordri  8586  oaordex  8594  odi  8615  pssnn  9206  alephval3  10147  dfac2b  10168  axdc4lem  10492  leexp1a  14211  wrdsymb0  14583  coprmproddvds  16696  lmodvsmmulgdi  20911  assamulgscm  21938  2ndcctbss  23478  2pthnloop  29763  wwlksnext  29922  frgrregord013  30423  atcvatlem  32413  umgr2cycllem  35124  exp5g  36285  cdleme48gfv1  40518  cdlemg6e  40604  dihord5apre  41244  dihglblem5apreN  41273  iccpartgt  47351  lmodvsmdi  48223  nn0sumshdiglemB  48469
  Copyright terms: Public domain W3C validator