Theorem imp4c 366

Description: An importation inference.

Hypothesis

Ref	Expression
imp4.1	|- (ph -> (ps -> (ch -> (th -> ta))))

Assertion

Ref	Expression
imp4c	|- (ph -> (((ps /\ ch) /\ th) -> ta))

Proof of Theorem imp4c

Step	Hyp	Ref	Expression
1		imp4.1	. . 3 |- (ph -> (ps -> (ch -> (th -> ta))))
2	1	imp3a 361	. 2 |- (ph -> ((ps /\ ch) -> (th -> ta)))
3	2	imp3a 361	1 |- (ph -> (((ps /\ ch) /\ th) -> ta))

Syntax hints:   -> wi 3   /\ wa 223

This theorem is referenced by:  imp44 371  omordi 4194  omwordri 4200  omass 4208  oewordri 4216  reclem4pr 5146  mulgt0sr 5201  seqzrn 6507  fsumsplit 6988  lmcau 7979  bcthlem29 8010  spanun 9455  elspansn5t 9487  atcvat3 10314  mdsymlem5 10325  sumdmdlem 10336

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