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

Theorem imp4b 422
Description: An importation inference. (Contributed by NM, 26-Apr-1994.) Shorten imp4a 423. (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 407 . 2 ((𝜑𝜓) → (𝜒 → (𝜃𝜏)))
32impd 411 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:  imp4a  423  imp43  428  imp5g  442  pm2.61da3ne  3103  onmindif  6273  oaordex  8173  pssnn  8724  alephval3  9524  dfac5  9542  dfac2b  9544  coftr  9683  zorn2lem6  9911  addcanpi  10309  mulcanpi  10310  ltmpi  10314  ltexprlem6  10451  axpre-sup  10579  bndndx  11884  relexpaddd  14401  dmdprdd  19050  lssssr  19654  coe1fzgsumdlem  20397  evl1gsumdlem  20447  1stcrest  21989  upgrreslem  27013  umgrreslem  27014  mdsymlem3  30109  mdsymlem6  30112  sumdmdlem  30122  mclsax  32713  mclsppslem  32727  prtlem17  35892  cvratlem  36437  paddidm  36857  pmodlem2  36863  pclfinclN  36966  icceuelpart  43473
  Copyright terms: Public domain W3C validator