Theorem 3imp 1224

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 1011	. 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 )

This proof depends on syntax axioms:   -> wi 4   /\ wa 104   /\ w3a 1009

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107

This proof depends on definitions:  df-bi 117  df-3an 1011

This theorem is used by:  3impa  1225  3imp31  1227  3imp231  1228  3impb  1230  3impia  1231  3impib  1232  3com23  1240  3an1rs  1250  3imp1  1251  3impd  1252  syl3an2  1312  syl3an3  1313  3jao  1342  biimp3ar  1387  f1ssf1  5674  poxp  6472  fvn0elsuppb  6496  suppfnss  6501  tfrlemibxssdm  6603  tfr1onlembxssdm  6619  tfrcllembxssdm  6632  nndi  6764  nnmass  6765  pr2nelem  7543  xnn0lenn0nn0  10283  difelfzle  10557  fzo1fzo0n0  10611  elfzo0z  10612  fzofzim  10616  elfzodifsumelfzo  10635  mulexp  11035  expadd  11038  expmul  11041  bernneq  11118  facdiv  11197  pfxfv  11477  swrdswrdlem  11497  pfxccat3  11527  reuccatpfxs1lem  11539  dvdsaddre2b  12632  addmodlteqALT  12650  ltoddhalfle  12684  halfleoddlt  12685  dfgcd2  12815  cncongr1  12905  oddprmgt2  12937  prmfac1  12955  infpnlem1  13166  dfgrp3me  13963  mulgaddcom  14007  mulginvcom  14008  assamulgscm  15151  fiinopn  15247  opnneissb  15398  blssps  15670  blss  15671  bcmono  16321  gausslemma2dlem1a  16399  2sqlem10  16466  ausgrumgrien  16633  ausgrusgrien  16634  ushgredgedg  16689  ushgredgedgloop  16691  edg0usgr  16710  0uhgrsubgr  16728  subumgredg2en  16734  wlkl1loop  16821  clwwlkccatlem  16863  umgrclwwlkge2  16865  clwwlkn1loopb  16883  clwwlkext2edg  16885  clwwlknonex2lem2  16901  clwwlknonex2  16902  clwwlknonex2e  16903  eupth2lem3lem6fi  16934