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

Theorem imp43 414
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 408 . 2 ((𝜑𝜓) → ((𝜒𝜃) → 𝜏))
32imp 393 1 (((𝜑𝜓) ∧ (𝜒𝜃)) → 𝜏)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 382
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 383
This theorem is referenced by:  fundmen  8187  fiint  8397  ltexprlem6  10069  divgt0  11097  divge0  11098  le2sq2  13146  iscatd  16541  isfuncd  16732  islmodd  19079  lmodvsghm  19134  islssd  19146  basis2  20976  neindisj  21142  dvidlem  23899  spansneleq  28769  elspansn4  28772  adjmul  29291  kbass6  29320  mdsl0  29509  chirredlem1  29589  poimirlem29  33771  rngonegmn1r  34073  3dim1  35276  linepsubN  35561  pmapsub  35577  tgoldbach  42230  tgoldbachOLD  42237
  Copyright terms: Public domain W3C validator