Theorem 3imp 1256

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 1039	. 2 |- ( ( ph /\ ps /\ ch ) <-> ( ( ph /\ ps ) /\ ch ) )
2		3imp.1	. . 3 |- ( ph -> ( ps -> ( ch -> th ) ) )
3	2	imp31 448	. 2 |- ( ( ( ph /\ ps ) /\ ch ) -> th )
4	1, 3	sylbi 207	1 |- ( ( ph /\ ps /\ ch ) -> th )

Syntax hints:   -> wi 4   /\ wa 384   /\ w3a 1037

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 197  df-an 386  df-3an 1039

This theorem is referenced by:  3imp31  1257  3imp231  1258  3impa  1259  3impb  1260  3impia  1261  3impib  1262  3com23  1271  3imp21  1277  3an1rs  1279  3imp1  1280  3impd  1281  syl3an2  1360  syl3an3  1361  3jao  1389  biimp3ar  1433  3elpr2eq  4435  wefrc  5108  predpo  5698  f1ssf1  6168  fveqdmss  6354  poxp  7289  fvn0elsuppb  7312  smo11  7461  odi  7659  omass  7660  nndi  7703  nnmass  7704  undifixp  7944  isinf  8173  domunfican  8233  infssuni  8257  pr2nelem  8827  dfac8alem  8852  fin33i  9191  fin1a2lem10  9231  domtriomlem  9264  axdc3lem2  9273  axdc3lem4  9275  axdc4lem  9277  ttukeyg  9339  axdclem  9341  grupr  9619  nqereu  9751  squeeze0  10926  rpnnen1lem5  11818  rpnnen1lem5OLD  11824  xnn0lenn0nn0  12075  supxrun  12146  difelfzle  12452  elfzo0z  12509  fzofzim  12514  fzo1fzo0n0  12518  elfzodifsumelfzo  12533  elfznelfzo  12573  injresinj  12589  mulexp  12899  expadd  12902  expmul  12905  bernneq  12990  facdiv  13074  hashgt12el2  13211  hashimarni  13228  leisorel  13244  fi1uzind  13279  fi1uzindOLD  13285  2swrd1eqwrdeq  13454  swrdswrdlem  13459  swrdccat3  13492  swrdccatid  13497  repswswrd  13531  cshf1  13556  2cshwcshw  13571  cshimadifsn  13575  swrdco  13583  relexpindlem  13803  dvdsaddre2b  15029  addmodlteqALT  15047  ltoddhalfle  15085  halfleoddlt  15086  dfgcd2  15263  coprmprod  15375  coprmproddvds  15377  cncongr1  15381  oddprmgt2  15411  prmfac1  15431  infpnlem1  15614  prmgaplem5  15759  prmgaplem6  15760  cshwshashlem1  15802  setsstruct  15898  iscatd2  16342  initoeu2lem2  16665  clatleglb  17126  dfgrp3e  17515  mulgaddcom  17564  mulginvcom  17565  symgfvne  17808  f1rhm0to0ALT  18741  lmodvsmmulgdi  18898  lsmcv  19141  assamulgscm  19350  psrvscafval  19390  mamufacex  20195  mat1scmat  20345  gsummatr01lem4  20464  cramer0  20496  chpscmat  20647  fvmptnn04ifa  20655  fvmptnn04ifc  20657  fvmptnn04ifd  20658  fiinopn  20706  opnneissb  20918  cnpimaex  21060  regsep  21138  hausnei2  21157  cmpsublem  21202  cmpsub  21203  filufint  21724  blssps  22229  blss  22230  mblsplit  23300  bcmono  25002  gausslemma2dlem1a  25090  2sqlem10  25153  upgrex  25987  numedglnl  26039  ausgrumgri  26062  ausgrusgri  26063  usgredg2vtxeuALT  26114  ushgredgedg  26121  ushgredgedgloop  26123  edg0usgr  26145  0uhgrsubgr  26171  subumgredg2  26177  fusgrfisbase  26220  cusgrsizeinds  26348  cusgrsize2inds  26349  finsumvtxdg2size  26446  upgrewlkle2  26502  wlkl1loop  26534  pthdivtx  26625  2pthnloop  26627  upgrwlkdvde  26633  uhgrwkspthlem2  26650  usgr2pthlem  26659  usgr2pth  26660  clwlkl1loop  26678  crctcshwlkn0lem4  26705  wwlksnextproplem3  26806  umgr2adedgwlkonALT  26843  umgr2wlk  26845  umgr2wlkon  26846  elwwlks2  26861  clwlkclwwlklem2  26901  umgrclwwlksge2  26912  clwwlksel  26914  clwwlksext2edg  26923  clwwnisshclwwsn  26930  1pthon2v  27013  uhgr3cyclex  27042  eupth2lem3lem6  27093  frgr3vlem1  27137  3cyclfrgrrn1  27149  frgrnbnb  27157  frgrwopreglem4a  27174  numclwwlkovf2exlem2  27212  numclwwlkovf2ex  27219  extwwlkfab  27223  frgrregord013  27253  frgrregord13  27254  frgrogt3nreg  27255  friendship  27257  chcompl  28099  spansncol  28427  hoaddsub  28675  bnj600  30989  sconnpht  31211  msubvrs  31457  funpsstri  31663  imp5p  32305  cntotbnd  33595  clmgmOLD  33650  grpomndo  33674  rngoneglmul  33742  rngonegrmul  33743  zerdivemp1x  33746  atlex  34603  cvlexch1  34615  cvlsupr4  34632  cvlsupr5  34633  cvlsupr6  34634  2llnneN  34695  athgt  34742  llnle  34804  lplnle  34826  lvoli2  34867  pmaple  35047  dalawlem10  35166  dalawlem13  35169  dalawlem14  35170  dalaw  35172  lhp2lt  35287  ldilval  35399  cdleme50trn2  35839  cdlemf  35851  cdlemg18b  35967  tendotp  36049  tendospcanN  36312  dihmeetlem3N  36594  dvh4dimlem  36732  pell14qrexpclnn0  37430  pell1qrgap  37438  aomclem2  37625  rngunsnply  37743  relexpxpmin  38009  relexpaddss  38010  rp-simp2  38087  gneispaceel2  38442  bi33imp12  38696  bi23imp13  38697  bi13imp23  38698  bi23imp1  38701  bi123imp0  38702  ee333  38713  jaoded  38782  e333  38960  suctrALTcf  39158  suctrALTcfVD  39159  ax6e2ndeqALT  39167  mullimc  39848  mullimcf  39855  fzopredsuc  41333  subsubelfzo0  41336  iccpartimp  41353  iccpartigtl  41359  lswn0  41380  pfxfv  41399  pfxccat3  41426  reuccatpfxs1lem  41433  fmtnofac1  41482  pwdif  41501  lighneallem2  41523  lighneallem3  41524  lighneallem4  41527  mogoldbblem  41629  gbegt5  41649  sbgoldbaltlem1  41667  bgoldbtbndlem2  41694  bgoldbtbndlem3  41695  lidldomn1  41921  cznnring  41956  rngccatidALTV  41989  ringccatidALTV  42052  scmsuppss  42153  lmodvsmdi  42163  gsumlsscl  42164  lindslinindimp2lem1  42247  lindsrng01  42257  elfzolborelfzop1  42309  difmodm1lt  42317  fllog2  42362  dignn0flhalflem1  42409