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  6318  tfrlemibxssdm  6413  tfr1onlembxssdm  6429  tfrcllembxssdm  6442  nndi  6572  nnmass  6573  pr2nelem  7299  xnn0lenn0nn0  9987  difelfzle  10256  fzo1fzo0n0  10307  elfzo0z  10308  fzofzim  10312  elfzodifsumelfzo  10330  mulexp  10723  expadd  10726  expmul  10729  bernneq  10805  facdiv  10883  dvdsaddre2b  12152  addmodlteqALT  12170  ltoddhalfle  12204  halfleoddlt  12205  dfgcd2  12335  cncongr1  12425  oddprmgt2  12456  prmfac1  12474  infpnlem1  12682  dfgrp3me  13432  mulgaddcom  13482  mulginvcom  13483  fiinopn  14476  opnneissb  14627  blssps  14899  blss  14900  gausslemma2dlem1a  15535  2sqlem10  15602