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

Step	Hyp	Ref	Expression
1		imp4.1	. . 3 |- (ph -> (ps -> (ch -> (th -> ta))))
2	1	imp4a 364	. 2 |- (ph -> (ps -> ((ch /\ th) -> ta)))
3	2	imp 350	1 |- ((ph /\ ps) -> ((ch /\ th) -> ta))

Syntax hints:   -> wi 3   /\ wa 223

This theorem is referenced by:  imp43 370  prth 555  onmindif 3055  eqfnfv 3788  oaordex 4182  nnaordex 4239  nnawordex 4240  pssnn 4519  aceq5 4720  aceq6b 4722  zorn2lem6 4773  alephval3 4883  mulcanpi 5007  ltmpi 5011  genpcd 5089  ltexprlem6 5127  ltexprlem7 5128  reclem3pr 5138  bndndx 6028  iooval2t 6312  basgen2t 7589  blssex 7806  metelcls 7916  mdsymlem3 10269  mdsymlem6 10272  sumdmdlem 10281  cmphmia 10606  cmphmib 10607  iri 10608

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