MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  imp43 Structured version   Visualization version   GIF version

Theorem imp43 622
Description: An importation inference. (Contributed by NM, 26-Apr-1994.)
Hypothesis
Ref Expression
imp4.1 (𝜑 → (𝜓 → (𝜒 → (𝜃𝜏))))
Assertion
Ref Expression
imp43 (((𝜑𝜓) ∧ (𝜒𝜃)) → 𝜏)

Proof of Theorem imp43
StepHypRef Expression
1 imp4.1 . . 3 (𝜑 → (𝜓 → (𝜒 → (𝜃𝜏))))
21imp4b 614 . 2 ((𝜑𝜓) → ((𝜒𝜃) → 𝜏))
32imp 444 1 (((𝜑𝜓) ∧ (𝜒𝜃)) → 𝜏)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 383
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 197  df-an 385
This theorem is referenced by:  fundmen  8195  fiint  8402  ltexprlem6  10055  divgt0  11083  divge0  11084  le2sq2  13133  iscatd  16535  isfuncd  16726  islmodd  19071  lmodvsghm  19126  islssd  19138  basis2  20957  neindisj  21123  dvidlem  23878  spansneleq  28738  elspansn4  28741  adjmul  29260  kbass6  29289  mdsl0  29478  chirredlem1  29558  poimirlem29  33751  rngonegmn1r  34054  3dim1  35256  linepsubN  35541  pmapsub  35557  tgoldbach  42215  tgoldbachOLD  42222
  Copyright terms: Public domain W3C validator