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  8588  oaordex  8596  odi  8617  pssnn  9208  alephval3  10150  dfac2b  10171  axdc4lem  10495  leexp1a  14215  wrdsymb0  14587  coprmproddvds  16700  lmodvsmmulgdi  20895  assamulgscm  21921  2ndcctbss  23463  2pthnloop  29751  wwlksnext  29913  frgrregord013  30414  atcvatlem  32404  umgr2cycllem  35145  exp5g  36304  cdleme48gfv1  40538  cdlemg6e  40624  dihord5apre  41264  dihglblem5apreN  41293  iccpartgt  47414  lmodvsmdi  48295  nn0sumshdiglemB  48541
  Copyright terms: Public domain W3C validator