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

Theorem imp4b 612
Description: An importation inference. (Contributed by NM, 26-Apr-1994.) Shorten imp4a 613. (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 445 . 2 ((𝜑𝜓) → (𝜒 → (𝜃𝜏)))
32impd 447 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 197  df-an 386
This theorem is referenced by:  imp4a  613  imp43  620  pm2.61da3ne  2879  onmindif  5784  oaordex  7598  pssnn  8138  alephval3  8893  dfac5  8911  dfac2  8913  coftr  9055  zorn2lem6  9283  addcanpi  9681  mulcanpi  9682  ltmpi  9686  ltexprlem6  9823  axpre-sup  9950  bndndx  11251  relexpaddd  13744  dmdprdd  18338  lssssr  18893  coe1fzgsumdlem  19611  evl1gsumdlem  19660  1stcrest  21196  mdsymlem3  29152  mdsymlem6  29155  sumdmdlem  29165  mclsax  31227  mclsppslem  31241  prtlem17  33680  cvratlem  34226  paddidm  34646  pmodlem2  34652  pclfinclN  34755  icceuelpart  40700
  Copyright terms: Public domain W3C validator