Theorem 3imp 1196

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

Syntax hints:   -> wi 4   /\ wa 104   /\ w3a 981

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

This theorem depends on definitions:  df-bi 117  df-3an 983

This theorem is referenced by:  3impa  1197  3imp31  1199  3imp231  1200  3impb  1202  3impia  1203  3impib  1204  3com23  1212  3an1rs  1222  3imp1  1223  3impd  1224  syl3an2  1284  syl3an3  1285  3jao  1314  biimp3ar  1359  poxp  6341  tfrlemibxssdm  6436  tfr1onlembxssdm  6452  tfrcllembxssdm  6465  nndi  6595  nnmass  6596  pr2nelem  7325  xnn0lenn0nn0  10022  difelfzle  10291  fzo1fzo0n0  10344  elfzo0z  10345  fzofzim  10349  elfzodifsumelfzo  10367  mulexp  10760  expadd  10763  expmul  10766  bernneq  10842  facdiv  10920  pfxfv  11175  swrdswrdlem  11195  pfxccat3  11225  reuccatpfxs1lem  11237  dvdsaddre2b  12267  addmodlteqALT  12285  ltoddhalfle  12319  halfleoddlt  12320  dfgcd2  12450  cncongr1  12540  oddprmgt2  12571  prmfac1  12589  infpnlem1  12797  dfgrp3me  13547  mulgaddcom  13597  mulginvcom  13598  fiinopn  14591  opnneissb  14742  blssps  15014  blss  15015  gausslemma2dlem1a  15650  2sqlem10  15717