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

Theorem imp43 416
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 410 . 2 ((𝜑𝜓) → ((𝜒𝜃) → 𝜏))
32imp 395 1 (((𝜑𝜓) ∧ (𝜒𝜃)) → 𝜏)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 384
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 198  df-an 385
This theorem is referenced by:  fundmen  8266  fiint  8476  ltexprlem6  10148  divgt0  11176  divge0  11177  le2sq2  13162  iscatd  16538  isfuncd  16729  islmodd  19073  lmodvsghm  19128  islssd  19140  basis2  20969  neindisj  21135  dvidlem  23893  spansneleq  28757  elspansn4  28760  adjmul  29279  kbass6  29308  mdsl0  29497  chirredlem1  29577  poimirlem29  33751  rngonegmn1r  34052  3dim1  35247  linepsubN  35532  pmapsub  35548  tgoldbach  42280
  Copyright terms: Public domain W3C validator