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 3056  eqfnfv 3792  oaordex 4185  nnaordex 4242  nnawordex 4243  pssnn 4522  aceq5 4723  aceq6b 4725  zorn2lem6 4776  alephval3 4886  mulcanpi 5010  ltmpi 5014  genpcd 5092  ltexprlem6 5130  ltexprlem7 5131  reclem3pr 5141  bndndx 6030  iooval2t 6317  basgen2t 7599  blssex 7816  metelcls 7927  mdsymlem3 10288  mdsymlem6 10291  sumdmdlem 10301  cmphmia 10642  cmphmib 10643  iri 10644

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