Theorem 3imp 1188

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 975	. 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 973

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 975

This theorem is referenced by:  3impa  1189  3imp31  1191  3imp231  1192  3impb  1194  3impia  1195  3impib  1196  3com23  1204  3an1rs  1214  3imp1  1215  3impd  1216  syl3an2  1267  syl3an3  1268  3jao  1296  biimp3ar  1341  poxp  6211  tfrlemibxssdm  6306  tfr1onlembxssdm  6322  tfrcllembxssdm  6335  nndi  6465  nnmass  6466  pr2nelem  7168  xnn0lenn0nn0  9822  difelfzle  10090  fzo1fzo0n0  10139  elfzo0z  10140  fzofzim  10144  elfzodifsumelfzo  10157  mulexp  10515  expadd  10518  expmul  10521  bernneq  10596  facdiv  10672  addmodlteqALT  11819  ltoddhalfle  11852  halfleoddlt  11853  dfgcd2  11969  cncongr1  12057  oddprmgt2  12088  prmfac1  12106  infpnlem1  12311  fiinopn  12796  opnneissb  12949  blssps  13221  blss  13222  2sqlem10  13755