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  5671  poxp  6468  fvn0elsuppb  6492  suppfnss  6497  tfrlemibxssdm  6598  tfr1onlembxssdm  6614  tfrcllembxssdm  6627  nndi  6759  nnmass  6760  pr2nelem  7537  xnn0lenn0nn0  10267  difelfzle  10541  fzo1fzo0n0  10595  elfzo0z  10596  fzofzim  10600  elfzodifsumelfzo  10619  mulexp  11015  expadd  11018  expmul  11021  bernneq  11098  facdiv  11176  pfxfv  11456  swrdswrdlem  11476  pfxccat3  11506  reuccatpfxs1lem  11518  dvdsaddre2b  12608  addmodlteqALT  12626  ltoddhalfle  12660  halfleoddlt  12661  dfgcd2  12791  cncongr1  12881  oddprmgt2  12912  prmfac1  12930  infpnlem1  13138  dfgrp3me  13905  mulgaddcom  13949  mulginvcom  13950  assamulgscm  15043  fiinopn  15105  opnneissb  15256  blssps  15528  blss  15529  gausslemma2dlem1a  16177  2sqlem10  16244  ausgrumgrien  16411  ausgrusgrien  16412  ushgredgedg  16467  ushgredgedgloop  16469  edg0usgr  16488  0uhgrsubgr  16506  subumgredg2en  16512  wlkl1loop  16599  clwwlkccatlem  16641  umgrclwwlkge2  16643  clwwlkn1loopb  16661  clwwlkext2edg  16663  clwwlknonex2lem2  16679  clwwlknonex2  16680  clwwlknonex2e  16681  eupth2lem3lem6fi  16712