Theorem imp31 280

Description: An importation inference.

Hypothesis

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

Assertion

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

Proof of Theorem imp31

Step	Hyp	Ref	Expression
1		imp3.1	. . 3 |- (ph -> (ps -> (ch -> th)))
2	1	imp 277	. 2 |- ((ph /\ ps) -> (ch -> th))
3	2	imp 277	1 |- (((ph /\ ps) /\ ch) -> th)

Syntax hints:   -> wi 2   /\ wa 196

This theorem is referenced by:  imp41 286  anassrs 338  3imp 608  3expa 612  pwssun 1917  ordelord 2221  tz7.7 2224  onint 2261  limsssuc 2362  findsg 2398  tfindsg 2402  weinxp 2467  fvco2 2866  isomin 2937  tfrlem1 2949  tfrlem9 2957  oelim 3137  oecl 3140  oaordi 3148  oaass 3163  omordi 3164  oen0 3165  omsmolem 3195  sdomen2 3380  xpmapenlem4 3394  php3 3411  unblem1 3431  r1ord 3499  rankr1 3518  aceq5 3563  zornlem7 3609  mulcanpi 3821  ltexprlem7 3942  reclem3pr 3952  suplem1pr 3955  suppsr2 4017  suppsr3 4018  supsr 4025  sup3 4511  elnnz 4572  qbtwnre 4650  infxpidmlem12 4944  projlem26 5218  projlem28 5220  pjoml 5271  osumlem6 5535  mdsymlem5 5780  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