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

Theorem imp4b 614
Description: An importation inference. (Contributed by NM, 26-Apr-1994.) Shorten imp4a 615. (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 444 . 2 ((𝜑𝜓) → (𝜒 → (𝜃𝜏)))
32impd 446 1 ((𝜑𝜓) → ((𝜒𝜃) → 𝜏))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 383
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 385
This theorem is referenced by:  imp4a  615  imp43  622  pm2.61da3ne  3009  onmindif  5964  oaordex  7795  pssnn  8331  alephval3  9094  dfac5  9112  dfac2b  9114  dfac2OLD  9116  coftr  9258  zorn2lem6  9486  addcanpi  9884  mulcanpi  9885  ltmpi  9889  ltexprlem6  10026  axpre-sup  10153  bndndx  11454  relexpaddd  13964  dmdprdd  18569  lssssr  19126  coe1fzgsumdlem  19844  evl1gsumdlem  19893  1stcrest  21429  upgrreslem  26366  umgrreslem  26367  mdsymlem3  29544  mdsymlem6  29547  sumdmdlem  29557  mclsax  31744  mclsppslem  31758  prtlem17  34634  cvratlem  35179  paddidm  35599  pmodlem2  35605  pclfinclN  35708  icceuelpart  41851
  Copyright terms: Public domain W3C validator