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  5671  poxp  6468  fvn0elsuppb  6492  suppfnss  6497  tfrlemibxssdm  6598  tfr1onlembxssdm  6614  tfrcllembxssdm  6627  nndi  6759  nnmass  6760  pr2nelem  7538  xnn0lenn0nn0  10278  difelfzle  10552  fzo1fzo0n0  10606  elfzo0z  10607  fzofzim  10611  elfzodifsumelfzo  10630  mulexp  11030  expadd  11033  expmul  11036  bernneq  11113  facdiv  11192  pfxfv  11472  swrdswrdlem  11492  pfxccat3  11522  reuccatpfxs1lem  11534  dvdsaddre2b  12627  addmodlteqALT  12645  ltoddhalfle  12679  halfleoddlt  12680  dfgcd2  12810  cncongr1  12900  oddprmgt2  12932  prmfac1  12950  infpnlem1  13161  dfgrp3me  13958  mulgaddcom  14002  mulginvcom  14003  assamulgscm  15127  fiinopn  15196  opnneissb  15347  blssps  15619  blss  15620  bcmono  16265  gausslemma2dlem1a  16343  2sqlem10  16410  ausgrumgrien  16577  ausgrusgrien  16578  ushgredgedg  16633  ushgredgedgloop  16635  edg0usgr  16654  0uhgrsubgr  16672  subumgredg2en  16678  wlkl1loop  16765  clwwlkccatlem  16807  umgrclwwlkge2  16809  clwwlkn1loopb  16827  clwwlkext2edg  16829  clwwlknonex2lem2  16845  clwwlknonex2  16846  clwwlknonex2e  16847  eupth2lem3lem6fi  16878