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

Theorem imp43 618
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 610 . 2 ((𝜑𝜓) → ((𝜒𝜃) → 𝜏))
32imp 443 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 195  df-an 384
This theorem is referenced by:  fundmen  7889  fiint  8095  ltexprlem6  9715  divgt0  10736  divge0  10737  le2sq2  12752  iscatd  16099  isfuncd  16290  islmodd  18634  lmodvsghm  18689  islssd  18699  basis2  20504  neindisj  20669  dvidlem  23398  spansneleq  27615  elspansn4  27618  adjmul  28137  kbass6  28166  mdsl0  28355  chirredlem1  28435  poimirlem29  32407  rngonegmn1r  32710  3dim1  33570  linepsubN  33855  pmapsub  33871  tgoldbach  40033  tgoldbachOLD  40040
  Copyright terms: Public domain W3C validator