Theorem imp4b 283

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

Syntax hints:   -> wi 2   /\ wa 196

This theorem is referenced by:  imp43 288  prth 429  onmindif 2312  cleqfv 2880  oaordex 3160  nnaordex 3191  nnawordex 3192  pssnn 3428  aceq5 3563  aceq6b 3565  zornlem6 3608  mulcanpi 3821  ltmpi 3825  genpcd 3903  ltexprlem6 3941  ltexprlem7 3942  reclem3pr 3952  mdsymlem3 5778  mdsymlem6 5781  sumdmdlem 5786

This theorem was proved from axioms:  ax-1 3  ax-2 4  ax-3 5  ax-mp 6

This theorem depends on definitions:  df-bi 128  df-an 198

metamath.org