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  8535  oaordex  8543  odi  8564  pssnn  9153  pssnnOLD  9250  alephval3  10089  dfac2b  10109  axdc4lem  10434  leexp1a  14124  wrdsymb0  14483  coprmproddvds  16584  lmodvsmmulgdi  20458  assamulgscm  21388  2ndcctbss  22890  2pthnloop  28917  wwlksnext  29076  frgrregord013  29577  atcvatlem  31565  umgr2cycllem  34026  exp5g  35056  cdleme48gfv1  39276  cdlemg6e  39362  dihord5apre  40002  dihglblem5apreN  40031  iccpartgt  45931  lmodvsmdi  46770  nn0sumshdiglemB  47018
  Copyright terms: Public domain W3C validator