Theorem 3imp 1097

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 886	. 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 884

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 886

This theorem is referenced by:  3impa  1098  3impb  1099  3impia  1100  3impib  1101  3com23  1109  3an1rs  1115  3imp1  1116  3impd  1117  syl3an2  1168  syl3an3  1169  3jao  1195  biimp3ar  1235  poxp  5794  tfrlemibxssdm  5882  nndi  6004  nnmass  6005  difelfzle  8762  fzo1fzo0n0  8809  elfzo0z  8810  fzofzim  8814  elfzodifsumelfzo  8827  mulexp  8948  expadd  8951  expmul  8954  bernneq  9022