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

Theorem imp4b 420
Description: An importation inference. (Contributed by NM, 26-Apr-1994.) Shorten imp4a 421. (Revised by Wolf Lammen, 19-Jul-2021.)
Hypothesis
Ref Expression
imp4.1 (𝜑 → (𝜓 → (𝜒 → (𝜃𝜏))))
Assertion
Ref Expression
imp4b ((𝜑𝜓) → ((𝜒𝜃) → 𝜏))

Proof of Theorem imp4b
StepHypRef Expression
1 imp4.1 . . 3 (𝜑 → (𝜓 → (𝜒 → (𝜃𝜏))))
21imp 405 . 2 ((𝜑𝜓) → (𝜒 → (𝜃𝜏)))
32impd 409 1 ((𝜑𝜓) → ((𝜒𝜃) → 𝜏))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 394
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 206  df-an 395
This theorem is referenced by:  imp4a  421  imp43  426  imp5g  440  pm2.61da3ne  3020  onmindif  6463  oaordex  8579  pssnn  9196  pssnnOLD  9293  alephval3  10140  dfac5  10158  dfac2b  10160  coftr  10303  zorn2lem6  10531  addcanpi  10929  mulcanpi  10930  ltmpi  10934  ltexprlem6  11071  axpre-sup  11199  bndndx  12509  dmdprdd  19973  lssssr  20855  coe1fzgsumdlem  22252  evl1gsumdlem  22305  1stcrest  23406  upgrreslem  29194  umgrreslem  29195  mdsymlem3  32292  mdsymlem6  32295  sumdmdlem  32305  mclsax  35312  mclsppslem  35326  disjlem17  38403  prtlem17  38480  cvratlem  39026  paddidm  39446  pmodlem2  39452  pclfinclN  39555  onexoegt  42816  icceuelpart  46915
  Copyright terms: Public domain W3C validator