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

Theorem imp43 428
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 422 . 2 ((𝜑𝜓) → ((𝜒𝜃) → 𝜏))
32imp 407 1 (((𝜑𝜓) ∧ (𝜒𝜃)) → 𝜏)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 396
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 208  df-an 397
This theorem is referenced by:  fundmen  8577  fiint  8789  ltexprlem6  10457  divgt0  11502  divge0  11503  le2sq2  13495  iscatd  16939  isfuncd  17130  islmodd  19576  lmodvsghm  19631  islssd  19643  basis2  21494  neindisj  21660  dvidlem  24447  spansneleq  29280  elspansn4  29283  adjmul  29802  kbass6  29831  mdsl0  30020  chirredlem1  30100  poimirlem29  34807  rngonegmn1r  35107  3dim1  36489  linepsubN  36774  pmapsub  36790  tgoldbach  43833
  Copyright terms: Public domain W3C validator