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  6169  tfrlemibxssdm  6264  tfr1onlembxssdm  6280  tfrcllembxssdm  6293  nndi  6422  nnmass  6423  pr2nelem  7105  xnn0lenn0nn0  9747  difelfzle  10011  fzo1fzo0n0  10060  elfzo0z  10061  fzofzim  10065  elfzodifsumelfzo  10078  mulexp  10436  expadd  10439  expmul  10442  bernneq  10516  facdiv  10589  addmodlteqALT  11724  ltoddhalfle  11757  halfleoddlt  11758  dfgcd2  11869  cncongr1  11951  oddprmgt2  11981  prmfac1  11997  fiinopn  12341  opnneissb  12494  blssps  12766  blss  12767