HomeHome Metamath Proof Explorer < Previous   Next >
Related theorems
Unicode version
Theorem imp4b 365
Description: An importation inference.
Hypothesis
Ref Expression
imp4.1 |- (ph -> (ps -> (ch -> (th -> ta))))
Assertion
Ref Expression
imp4b |- ((ph /\ ps) -> ((ch /\ th) -> ta))
Proof of Theorem imp4b
StepHypRef Expression
1 imp4.1 . . 3 |- (ph -> (ps -> (ch -> (th -> ta))))
21imp4a 364 . 2 |- (ph -> (ps -> ((ch /\ th) -> ta)))
32imp 350 1 |- ((ph /\ ps) -> ((ch /\ th) -> ta))
Colors of variables: wff set class
Syntax hints:   -> wi 3   /\ wa 223
This theorem is referenced by:  imp43 370  prth 554  onmindif 3050  eqfnfv 3782  oaordex 4176  nnaordex 4233  nnawordex 4234  pssnn 4513  aceq5 4712  aceq6b 4714  zorn2lem6 4765  alephval3 4875  mulcanpi 4999  ltmpi 5003  genpcd 5081  ltexprlem6 5119  ltexprlem7 5120  reclem3pr 5130  bndndx 6020  iooval2t 6304  basgen2t 7581  blssex 7794  metelcls 7900  mdsymlem3 10240  mdsymlem6 10243  sumdmdlem 10252  cmphmia 10570  cmphmib 10571  iri 10572
This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7
This theorem depends on definitions:  df-bi 147  df-an 225
Copyright terms: Public domain