Theorem 3imp 1217

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 1004	. 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 1002

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 1004

This theorem is referenced by:  3impa  1218  3imp31  1220  3imp231  1221  3impb  1223  3impia  1224  3impib  1225  3com23  1233  3an1rs  1243  3imp1  1244  3impd  1245  syl3an2  1305  syl3an3  1306  3jao  1335  biimp3ar  1380  poxp  6384  tfrlemibxssdm  6479  tfr1onlembxssdm  6495  tfrcllembxssdm  6508  nndi  6640  nnmass  6641  pr2nelem  7375  xnn0lenn0nn0  10073  difelfzle  10342  fzo1fzo0n0  10395  elfzo0z  10396  fzofzim  10400  elfzodifsumelfzo  10419  mulexp  10812  expadd  10815  expmul  10818  bernneq  10894  facdiv  10972  pfxfv  11231  swrdswrdlem  11251  pfxccat3  11281  reuccatpfxs1lem  11293  dvdsaddre2b  12367  addmodlteqALT  12385  ltoddhalfle  12419  halfleoddlt  12420  dfgcd2  12550  cncongr1  12640  oddprmgt2  12671  prmfac1  12689  infpnlem1  12897  dfgrp3me  13648  mulgaddcom  13698  mulginvcom  13699  fiinopn  14693  opnneissb  14844  blssps  15116  blss  15117  gausslemma2dlem1a  15752  2sqlem10  15819  ausgrumgrien  15983  ausgrusgrien  15984  ushgredgedg  16039  ushgredgedgloop  16041  wlkl1loop  16099  clwwlkccatlem  16137  umgrclwwlkge2  16139