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  5779  oaordex  7590  pssnn  8130  alephval3  8885  dfac5  8903  dfac2  8905  coftr  9047  zorn2lem6  9275  addcanpi  9673  mulcanpi  9674  ltmpi  9678  ltexprlem6  9815  axpre-sup  9942  bndndx  11243  relexpaddd  13736  dmdprdd  18330  lssssr  18885  coe1fzgsumdlem  19603  evl1gsumdlem  19652  1stcrest  21179  mdsymlem3  29134  mdsymlem6  29137  sumdmdlem  29147  mclsax  31209  mclsppslem  31223  prtlem17  33676  cvratlem  34222  paddidm  34642  pmodlem2  34648  pclfinclN  34751  icceuelpart  40696
  Copyright terms: Public domain W3C validator