Theorem 3imp 1175

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 964	. 2 |- ( ( ph /\ ps /\ ch ) <-> ( ( ph /\ ps ) /\ ch ) )
2		3imp.1	. . 3 |- ( ph -> ( ps -> ( ch -> th ) ) )
3	2	imp31 254	. 2 |- ( ( ( ph /\ ps ) /\ ch ) -> th )
4	1, 3	sylbi 120	1 |- ( ( ph /\ ps /\ ch ) -> th )

Syntax hints:   -> wi 4   /\ wa 103   /\ w3a 962

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

This theorem depends on definitions:  df-bi 116  df-3an 964

This theorem is referenced by:  3impa  1176  3impb  1177  3impia  1178  3impib  1179  3com23  1187  3an1rs  1197  3imp1  1198  3impd  1199  syl3an2  1250  syl3an3  1251  3jao  1279  biimp3ar  1324  poxp  6122  tfrlemibxssdm  6217  tfr1onlembxssdm  6233  tfrcllembxssdm  6246  nndi  6375  nnmass  6376  pr2nelem  7040  xnn0lenn0nn0  9641  difelfzle  9904  fzo1fzo0n0  9953  elfzo0z  9954  fzofzim  9958  elfzodifsumelfzo  9971  mulexp  10325  expadd  10328  expmul  10331  bernneq  10405  facdiv  10477  addmodlteqALT  11546  ltoddhalfle  11579  halfleoddlt  11580  dfgcd2  11691  cncongr1  11773  oddprmgt2  11803  prmfac1  11819  fiinopn  12160  opnneissb  12313  blssps  12585  blss  12586