Theorem 3imp 1220

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 1007	. 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 1005

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 1007

This theorem is referenced by:  3impa  1221  3imp31  1223  3imp231  1224  3impb  1226  3impia  1227  3impib  1228  3com23  1236  3an1rs  1246  3imp1  1247  3impd  1248  syl3an2  1308  syl3an3  1309  3jao  1338  biimp3ar  1383  f1ssf1  5624  poxp  6406  fvn0elsuppb  6430  suppfnss  6435  tfrlemibxssdm  6536  tfr1onlembxssdm  6552  tfrcllembxssdm  6565  nndi  6697  nnmass  6698  pr2nelem  7439  xnn0lenn0nn0  10144  difelfzle  10414  fzo1fzo0n0  10468  elfzo0z  10469  fzofzim  10473  elfzodifsumelfzo  10492  mulexp  10886  expadd  10889  expmul  10892  bernneq  10968  facdiv  11046  pfxfv  11314  swrdswrdlem  11334  pfxccat3  11364  reuccatpfxs1lem  11376  dvdsaddre2b  12465  addmodlteqALT  12483  ltoddhalfle  12517  halfleoddlt  12518  dfgcd2  12648  cncongr1  12738  oddprmgt2  12769  prmfac1  12787  infpnlem1  12995  dfgrp3me  13746  mulgaddcom  13796  mulginvcom  13797  fiinopn  14798  opnneissb  14949  blssps  15221  blss  15222  gausslemma2dlem1a  15860  2sqlem10  15927  ausgrumgrien  16094  ausgrusgrien  16095  ushgredgedg  16150  ushgredgedgloop  16152  edg0usgr  16171  0uhgrsubgr  16189  subumgredg2en  16195  wlkl1loop  16282  clwwlkccatlem  16324  umgrclwwlkge2  16326  clwwlkn1loopb  16344  clwwlkext2edg  16346  clwwlknonex2lem2  16362  clwwlknonex2  16363  clwwlknonex2e  16364  eupth2lem3lem6fi  16395