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  3111  onmindif  6279  oaordex  8179  pssnn  8730  alephval3  9530  dfac5  9548  dfac2b  9550  coftr  9689  zorn2lem6  9917  addcanpi  10315  mulcanpi  10316  ltmpi  10320  ltexprlem6  10457  axpre-sup  10585  bndndx  11890  relexpaddd  14408  dmdprdd  19057  lssssr  19661  coe1fzgsumdlem  20404  evl1gsumdlem  20454  1stcrest  21996  upgrreslem  27019  umgrreslem  27020  mdsymlem3  30115  mdsymlem6  30118  sumdmdlem  30128  mclsax  32719  mclsppslem  32733  prtlem17  35898  cvratlem  36443  paddidm  36863  pmodlem2  36869  pclfinclN  36972  icceuelpart  43447
  Copyright terms: Public domain W3C validator