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

Theorem imp43 619
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 611 . 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 196  df-an 385
This theorem is referenced by:  fundmen  7916  fiint  8122  ltexprlem6  9742  divgt0  10770  divge0  10771  le2sq2  12801  iscatd  16157  isfuncd  16348  islmodd  18692  lmodvsghm  18747  islssd  18757  basis2  20566  neindisj  20731  dvidlem  23485  spansneleq  27813  elspansn4  27816  adjmul  28335  kbass6  28364  mdsl0  28553  chirredlem1  28633  poimirlem29  32608  rngonegmn1r  32911  3dim1  33771  linepsubN  34056  pmapsub  34072  tgoldbach  40232  tgoldbachOLD  40239
  Copyright terms: Public domain W3C validator