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  8017  oaordex  8025  odi  8046  pssnn  8572  alephval3  9371  dfac2b  9391  axdc4lem  9712  leexp1a  13377  wrdsymb0  13735  coprmproddvds  15824  lmodvsmmulgdi  19347  assamulgscm  19806  2ndcctbss  21735  2pthnloop  27187  wwlksnext  27346  frgrregord013  27854  atcvatlem  29841  umgr2cycllem  31951  exp5g  33205  cdleme48gfv1  37153  cdlemg6e  37239  dihord5apre  37879  dihglblem5apreN  37908  iccpartgt  43023  lmodvsmdi  43864  nn0sumshdiglemB  44115
  Copyright terms: Public domain W3C validator