Theorem 3imp 1176

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 965	. 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 963

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 965

This theorem is referenced by:  3impa  1177  3impb  1178  3impia  1179  3impib  1180  3com23  1188  3an1rs  1198  3imp1  1199  3impd  1200  syl3an2  1251  syl3an3  1252  3jao  1280  biimp3ar  1325  poxp  6137  tfrlemibxssdm  6232  tfr1onlembxssdm  6248  tfrcllembxssdm  6261  nndi  6390  nnmass  6391  pr2nelem  7064  xnn0lenn0nn0  9678  difelfzle  9942  fzo1fzo0n0  9991  elfzo0z  9992  fzofzim  9996  elfzodifsumelfzo  10009  mulexp  10363  expadd  10366  expmul  10369  bernneq  10443  facdiv  10516  addmodlteqALT  11593  ltoddhalfle  11626  halfleoddlt  11627  dfgcd2  11738  cncongr1  11820  oddprmgt2  11850  prmfac1  11866  fiinopn  12210  opnneissb  12363  blssps  12635  blss  12636