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  5646  poxp  6428  fvn0elsuppb  6452  suppfnss  6457  tfrlemibxssdm  6558  tfr1onlembxssdm  6574  tfrcllembxssdm  6587  nndi  6719  nnmass  6720  pr2nelem  7488  xnn0lenn0nn0  10198  difelfzle  10468  fzo1fzo0n0  10522  elfzo0z  10523  fzofzim  10527  elfzodifsumelfzo  10546  mulexp  10940  expadd  10943  expmul  10946  bernneq  11022  facdiv  11100  pfxfv  11376  swrdswrdlem  11396  pfxccat3  11426  reuccatpfxs1lem  11438  dvdsaddre2b  12527  addmodlteqALT  12545  ltoddhalfle  12579  halfleoddlt  12580  dfgcd2  12710  cncongr1  12800  oddprmgt2  12831  prmfac1  12849  infpnlem1  13057  dfgrp3me  13813  mulgaddcom  13863  mulginvcom  13864  fiinopn  14869  opnneissb  15020  blssps  15292  blss  15293  gausslemma2dlem1a  15931  2sqlem10  15998  ausgrumgrien  16165  ausgrusgrien  16166  ushgredgedg  16221  ushgredgedgloop  16223  edg0usgr  16242  0uhgrsubgr  16260  subumgredg2en  16266  wlkl1loop  16353  clwwlkccatlem  16395  umgrclwwlkge2  16397  clwwlkn1loopb  16415  clwwlkext2edg  16417  clwwlknonex2lem2  16433  clwwlknonex2  16434  clwwlknonex2e  16435  eupth2lem3lem6fi  16466