Theorem imp4a 282

Description: An importation inference.

Hypothesis

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

Assertion

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

Proof of Theorem imp4a

Step	Hyp	Ref	Expression
1		imp4.1	. 2 |- (ph -> (ps -> (ch -> (th -> ta ))))
2		impexp 276	. 2 |- (((ch /\ th) -> ta ) <-> (ch -> (th -> ta )))
3	1, 2	syl6ibr 186	1 |- (ph -> (ps -> ((ch /\ th) -> ta )))

Syntax hints:   -> wi 2   /\ wa 196

This theorem is referenced by:  imp4b 283  imp4d 285  wefrc 2195  f1oweOLD 2944  tfrlem1 2949  tfrlem9 2957  tz7.49 2997  oaordex 3160  aceq6b 3565  zornlem4 3606  zornlem7 3609  psslinpr 3929  prlem936 3949  atcvatlem 5770  atcvat4 5775

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