Theorem imp4b 363

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 362	. 2 |- (ph -> (ps -> ((ch /\ th) -> ta)))
3	2	imp 348	1 |- ((ph /\ ps) -> ((ch /\ th) -> ta))

Syntax hints:   -> wi 3   /\ wa 221

This theorem is referenced by:  imp43 368  prth 559  onmindif 3061  eqfnfv 3909  oaordex 4328  nnaordex 4389  nnawordex 4390  pssnn 4681  aceq5 4886  aceq6b 4888  zorn2lem6 4939  alephval3 5053  mulcanpi 5181  ltmpi 5185  genpcd 5263  ltexprlem6 5301  ltexprlem7 5302  reclem3pr 5312  bndndx 6241  iooval2 6493  basgen2 7851  blssex 8064  metelcls 8176  mdsymlem3 10614  mdsymlem6 10617  sumdmdlem 10627  ununr 10955  cmphmia 11253  cmphmib 11254  iri 11255  ordtypelem5 11431  neibastop2lem3 11582  topjoin 11588  fnejoin1 11591  fnejoin2 11592

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 145  df-an 223

Copyright terms: Public domain