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  5651  poxp  6441  fvn0elsuppb  6465  suppfnss  6470  tfrlemibxssdm  6571  tfr1onlembxssdm  6587  tfrcllembxssdm  6600  nndi  6732  nnmass  6733  pr2nelem  7501  xnn0lenn0nn0  10217  difelfzle  10490  fzo1fzo0n0  10544  elfzo0z  10545  fzofzim  10549  elfzodifsumelfzo  10568  mulexp  10964  expadd  10967  expmul  10970  bernneq  11047  facdiv  11125  pfxfv  11401  swrdswrdlem  11421  pfxccat3  11451  reuccatpfxs1lem  11463  dvdsaddre2b  12552  addmodlteqALT  12570  ltoddhalfle  12604  halfleoddlt  12605  dfgcd2  12735  cncongr1  12825  oddprmgt2  12856  prmfac1  12874  infpnlem1  13082  dfgrp3me  13855  mulgaddcom  13899  mulginvcom  13900  fiinopn  14995  opnneissb  15146  blssps  15418  blss  15419  gausslemma2dlem1a  16057  2sqlem10  16124  ausgrumgrien  16291  ausgrusgrien  16292  ushgredgedg  16347  ushgredgedgloop  16349  edg0usgr  16368  0uhgrsubgr  16386  subumgredg2en  16392  wlkl1loop  16479  clwwlkccatlem  16521  umgrclwwlkge2  16523  clwwlkn1loopb  16541  clwwlkext2edg  16543  clwwlknonex2lem2  16559  clwwlknonex2  16560  clwwlknonex2e  16561  eupth2lem3lem6fi  16592