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

Theorem imp43 426
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 420 . 2 ((𝜑𝜓) → ((𝜒𝜃) → 𝜏))
32imp 405 1 (((𝜑𝜓) ∧ (𝜒𝜃)) → 𝜏)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 394
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 395
This theorem is referenced by:  fundmen  9056  fiint  9350  ltexprlem6  11066  divgt0  12115  divge0  12116  le2sq2  14135  iscatd  17656  isfuncd  17854  islmodd  20761  lmodvsghm  20818  islssd  20831  basis2  22898  neindisj  23065  dvidlem  25888  spansneleq  31452  elspansn4  31455  adjmul  31974  kbass6  32003  mdsl0  32192  chirredlem1  32272  poimirlem29  37253  rngonegmn1r  37546  3dim1  39070  linepsubN  39355  pmapsub  39371  tgoldbach  47294
  Copyright terms: Public domain W3C validator