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 208  df-an 397
This theorem is referenced by:  exp5j  446  oawordri  8165  oaordex  8173  odi  8194  pssnn  8724  alephval3  9524  dfac2b  9544  axdc4lem  9865  leexp1a  13527  wrdsymb0  13889  coprmproddvds  15995  lmodvsmmulgdi  19598  assamulgscm  20058  2ndcctbss  21991  2pthnloop  27439  wwlksnext  27598  frgrregord013  28101  atcvatlem  30089  umgr2cycllem  32284  exp5g  33548  cdleme48gfv1  37552  cdlemg6e  37638  dihord5apre  38278  dihglblem5apreN  38307  iccpartgt  43464  lmodvsmdi  44358  nn0sumshdiglemB  44608
  Copyright terms: Public domain W3C validator