Theorem 3imp 1219

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 1006	. 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 1004

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 1006

This theorem is referenced by:  3impa  1220  3imp31  1222  3imp231  1223  3impb  1225  3impia  1226  3impib  1227  3com23  1235  3an1rs  1245  3imp1  1246  3impd  1247  syl3an2  1307  syl3an3  1308  3jao  1337  biimp3ar  1382  f1ssf1  5615  poxp  6396  tfrlemibxssdm  6492  tfr1onlembxssdm  6508  tfrcllembxssdm  6521  nndi  6653  nnmass  6654  pr2nelem  7395  xnn0lenn0nn0  10099  difelfzle  10368  fzo1fzo0n0  10421  elfzo0z  10422  fzofzim  10426  elfzodifsumelfzo  10445  mulexp  10839  expadd  10842  expmul  10845  bernneq  10921  facdiv  10999  pfxfv  11264  swrdswrdlem  11284  pfxccat3  11314  reuccatpfxs1lem  11326  dvdsaddre2b  12401  addmodlteqALT  12419  ltoddhalfle  12453  halfleoddlt  12454  dfgcd2  12584  cncongr1  12674  oddprmgt2  12705  prmfac1  12723  infpnlem1  12931  dfgrp3me  13682  mulgaddcom  13732  mulginvcom  13733  fiinopn  14727  opnneissb  14878  blssps  15150  blss  15151  gausslemma2dlem1a  15786  2sqlem10  15853  ausgrumgrien  16020  ausgrusgrien  16021  ushgredgedg  16076  ushgredgedgloop  16078  edg0usgr  16097  0uhgrsubgr  16115  subumgredg2en  16121  wlkl1loop  16208  clwwlkccatlem  16250  umgrclwwlkge2  16252  clwwlkn1loopb  16270  clwwlkext2edg  16272  clwwlknonex2lem2  16288  clwwlknonex2  16289  clwwlknonex2e  16290