Theorem 3imp 1224

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 1011	. 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 )

This proof depends on syntax axioms:   -> wi 4   /\ wa 104   /\ w3a 1009

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107

This proof depends on definitions:  df-bi 117  df-3an 1011

This theorem is used by:  3impa  1225  3imp31  1227  3imp231  1228  3impb  1230  3impia  1231  3impib  1232  3com23  1240  3an1rs  1250  3imp1  1251  3impd  1252  syl3an2  1312  syl3an3  1313  3jao  1342  biimp3ar  1387  f1ssf1  5674  poxp  6472  fvn0elsuppb  6496  suppfnss  6501  tfrlemibxssdm  6602  tfr1onlembxssdm  6618  tfrcllembxssdm  6631  nndi  6763  nnmass  6764  pr2nelem  7543  xnn0lenn0nn0  10284  difelfzle  10558  fzo1fzo0n0  10612  elfzo0z  10613  fzofzim  10617  elfzodifsumelfzo  10636  mulexp  11036  expadd  11039  expmul  11042  bernneq  11119  facdiv  11198  pfxfv  11478  swrdswrdlem  11498  pfxccat3  11528  reuccatpfxs1lem  11540  dvdsaddre2b  12633  addmodlteqALT  12651  ltoddhalfle  12685  halfleoddlt  12686  dfgcd2  12816  cncongr1  12906  oddprmgt2  12938  prmfac1  12956  infpnlem1  13167  dfgrp3me  13964  mulgaddcom  14008  mulginvcom  14009  assamulgscm  15152  fiinopn  15230  opnneissb  15381  blssps  15653  blss  15654  bcmono  16304  gausslemma2dlem1a  16382  2sqlem10  16449  ausgrumgrien  16616  ausgrusgrien  16617  ushgredgedg  16672  ushgredgedgloop  16674  edg0usgr  16693  0uhgrsubgr  16711  subumgredg2en  16717  wlkl1loop  16804  clwwlkccatlem  16846  umgrclwwlkge2  16848  clwwlkn1loopb  16866  clwwlkext2edg  16868  clwwlknonex2lem2  16884  clwwlknonex2  16885  clwwlknonex2e  16886  eupth2lem3lem6fi  16917