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  8381  oaordex  8389  odi  8410  pssnn  8951  pssnnOLD  9040  alephval3  9866  dfac2b  9886  axdc4lem  10211  leexp1a  13893  wrdsymb0  14252  coprmproddvds  16368  lmodvsmmulgdi  20158  assamulgscm  21105  2ndcctbss  22606  2pthnloop  28099  wwlksnext  28258  frgrregord013  28759  atcvatlem  30747  umgr2cycllem  33102  exp5g  34492  cdleme48gfv1  38550  cdlemg6e  38636  dihord5apre  39276  dihglblem5apreN  39305  iccpartgt  44879  lmodvsmdi  45718  nn0sumshdiglemB  45966
  Copyright terms: Public domain W3C validator