Theorem 3exp 611

Description: Exportation inference.

Hypothesis

Ref	Expression
3exp.1	|- ((ph /\ ps /\ ch) -> th)

Assertion

Ref	Expression
3exp	|- (ph -> (ps -> (ch -> th)))

Proof of Theorem 3exp

Step	Hyp	Ref	Expression
1		df-3an 583	. . 3 |- ((ph /\ ps /\ ch) <-> ((ph /\ ps) /\ ch))
2		3exp.1	. . 3 |- ((ph /\ ps /\ ch) -> th)
3	1, 2	sylbir 176	. 2 |- (((ph /\ ps) /\ ch) -> th)
4	3	exp31 293	1 |- (ph -> (ps -> (ch -> th)))

Syntax hints:   -> wi 2   /\ wa 196   /\ w3a 581

This theorem is referenced by:  3expa 612  3expb 613  3com12 614  3com23 616  syl3an2 620  syl3an3 621  rgen3 1265  3gencl 1367  vtocl3ga 1389  euuni 1954  ssorduni 2249  suceloni 2314  unizlim 2364  nnsuc 2389  tfinds 2401  sotri 2630  ndmord 3064  nndi 3180  nnmass 3181  3ecoptocl 3241  eceqopreq 3249  mapvalg 3263  mulcanpi 3821  ltmpi 3825  divasst 4239  uzwo3lem1 4614  qbtwnre 4650  sqrlem20 4750  projlem26 5218  omlsi 5250  spansneleq 5475  osumlem4 5533  strlem3a 5693  spansncv2t 5725

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  df-3an 583

metamath.org