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

Theorem imp43 427
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 421 . 2 ((𝜑𝜓) → ((𝜒𝜃) → 𝜏))
32imp 406 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:  fundmen  9071  fiint  9366  fiintOLD  9367  ltexprlem6  11081  divgt0  12136  divge0  12137  le2sq2  14175  iscatd  17716  isfuncd  17910  islmodd  20864  lmodvsghm  20921  islssd  20933  basis2  22958  neindisj  23125  dvidlem  25950  spansneleq  31589  elspansn4  31592  adjmul  32111  kbass6  32140  mdsl0  32329  chirredlem1  32409  r1peuqusdeg1  35648  poimirlem29  37656  rngonegmn1r  37949  3dim1  39469  linepsubN  39754  pmapsub  39770  tgoldbach  47804
  Copyright terms: Public domain W3C validator