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

Theorem imp4b 410
Description: An importation inference. (Contributed by NM, 26-Apr-1994.) Shorten imp4a 411. (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 395 . 2 ((𝜑𝜓) → (𝜒 → (𝜃𝜏)))
32impd 398 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:  imp4a  411  imp43  416  pm2.61da3ne  3078  onmindif  6040  oaordex  7885  pssnn  8427  alephval3  9226  dfac5  9244  dfac2b  9246  dfac2OLD  9248  coftr  9390  zorn2lem6  9618  addcanpi  10016  mulcanpi  10017  ltmpi  10021  ltexprlem6  10158  axpre-sup  10285  bndndx  11578  relexpaddd  14037  dmdprdd  18620  lssssr  19179  lssssrOLD  19180  coe1fzgsumdlem  19899  evl1gsumdlem  19948  1stcrest  21491  upgrreslem  26435  umgrreslem  26436  mdsymlem3  29615  mdsymlem6  29618  sumdmdlem  29628  mclsax  31811  mclsppslem  31825  prtlem17  34674  cvratlem  35220  paddidm  35640  pmodlem2  35646  pclfinclN  35749  icceuelpart  41965
  Copyright terms: Public domain W3C validator