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  10277  difelfzle  10551  fzo1fzo0n0  10605  elfzo0z  10606  fzofzim  10610  elfzodifsumelfzo  10629  mulexp  11028  expadd  11031  expmul  11034  bernneq  11111  facdiv  11190  pfxfv  11470  swrdswrdlem  11490  pfxccat3  11520  reuccatpfxs1lem  11532  dvdsaddre2b  12624  addmodlteqALT  12642  ltoddhalfle  12676  halfleoddlt  12677  dfgcd2  12807  cncongr1  12897  oddprmgt2  12929  prmfac1  12947  infpnlem1  13158  dfgrp3me  13954  mulgaddcom  13998  mulginvcom  13999  assamulgscm  15092  fiinopn  15154  opnneissb  15305  blssps  15577  blss  15578  bcmono  16202  gausslemma2dlem1a  16275  2sqlem10  16342  ausgrumgrien  16509  ausgrusgrien  16510  ushgredgedg  16565  ushgredgedgloop  16567  edg0usgr  16586  0uhgrsubgr  16604  subumgredg2en  16610  wlkl1loop  16697  clwwlkccatlem  16739  umgrclwwlkge2  16741  clwwlkn1loopb  16759  clwwlkext2edg  16761  clwwlknonex2lem2  16777  clwwlknonex2  16778  clwwlknonex2e  16779  eupth2lem3lem6fi  16810