Theorem 3imp 1183

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 970	. 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 968

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 970

This theorem is referenced by:  3impa  1184  3imp31  1186  3imp231  1187  3impb  1189  3impia  1190  3impib  1191  3com23  1199  3an1rs  1209  3imp1  1210  3impd  1211  syl3an2  1262  syl3an3  1263  3jao  1291  biimp3ar  1336  poxp  6200  tfrlemibxssdm  6295  tfr1onlembxssdm  6311  tfrcllembxssdm  6324  nndi  6454  nnmass  6455  pr2nelem  7147  xnn0lenn0nn0  9801  difelfzle  10069  fzo1fzo0n0  10118  elfzo0z  10119  fzofzim  10123  elfzodifsumelfzo  10136  mulexp  10494  expadd  10497  expmul  10500  bernneq  10575  facdiv  10651  addmodlteqALT  11797  ltoddhalfle  11830  halfleoddlt  11831  dfgcd2  11947  cncongr1  12035  oddprmgt2  12066  prmfac1  12084  infpnlem1  12289  fiinopn  12652  opnneissb  12805  blssps  13077  blss  13078  2sqlem10  13611