Theorem 3imp 1098

Description: Importation inference. (Contributed by NM, 8-Apr-1994.)

Hypothesis

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

Assertion

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

Proof of Theorem 3imp

Step	Hyp	Ref	Expression
1		df-3an 887	. 2 |- ( ( ph /\ ps /\ ch ) <-> ( ( ph /\ ps ) /\ ch ) )
2		3imp.1	. . 3 |- ( ph -> ( ps -> ( ch -> th ) ) )
3	2	imp31 243	. 2 |- ( ( ( ph /\ ps ) /\ ch ) -> th )
4	1, 3	sylbi 114	1 |- ( ( ph /\ ps /\ ch ) -> th )

Syntax hints:   -> wi 4   /\ wa 97   /\ w3a 885

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100

This theorem depends on definitions:  df-bi 110  df-3an 887

This theorem is referenced by:  3impa  1099  3impb  1100  3impia  1101  3impib  1102  3com23  1110  3an1rs  1116  3imp1  1117  3impd  1118  syl3an2  1169  syl3an3  1170  3jao  1196  biimp3ar  1236  poxp  5853  tfrlemibxssdm  5941  nndi  6065  nnmass  6066  difelfzle  8992  fzo1fzo0n0  9039  elfzo0z  9040  fzofzim  9044  elfzodifsumelfzo  9057  mulexp  9294  expadd  9297  expmul  9300  bernneq  9369