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 )

Syntax hints:   -> wi 4   /\ wa 104   /\ w3a 1009

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 1011

This theorem is referenced 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  5666  poxp  6458  fvn0elsuppb  6482  suppfnss  6487  tfrlemibxssdm  6588  tfr1onlembxssdm  6604  tfrcllembxssdm  6617  nndi  6749  nnmass  6750  pr2nelem  7527  xnn0lenn0nn0  10246  difelfzle  10519  fzo1fzo0n0  10573  elfzo0z  10574  fzofzim  10578  elfzodifsumelfzo  10597  mulexp  10993  expadd  10996  expmul  10999  bernneq  11076  facdiv  11154  pfxfv  11434  swrdswrdlem  11454  pfxccat3  11484  reuccatpfxs1lem  11496  dvdsaddre2b  12586  addmodlteqALT  12604  ltoddhalfle  12638  halfleoddlt  12639  dfgcd2  12769  cncongr1  12859  oddprmgt2  12890  prmfac1  12908  infpnlem1  13116  dfgrp3me  13882  mulgaddcom  13926  mulginvcom  13927  fiinopn  15028  opnneissb  15179  blssps  15451  blss  15452  gausslemma2dlem1a  16091  2sqlem10  16158  ausgrumgrien  16325  ausgrusgrien  16326  ushgredgedg  16381  ushgredgedgloop  16383  edg0usgr  16402  0uhgrsubgr  16420  subumgredg2en  16426  wlkl1loop  16513  clwwlkccatlem  16555  umgrclwwlkge2  16557  clwwlkn1loopb  16575  clwwlkext2edg  16577  clwwlknonex2lem2  16593  clwwlknonex2  16594  clwwlknonex2e  16595  eupth2lem3lem6fi  16626