Theorem 3imp 1217

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

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 1004

This theorem is referenced by:  3impa  1218  3imp31  1220  3imp231  1221  3impb  1223  3impia  1224  3impib  1225  3com23  1233  3an1rs  1243  3imp1  1244  3impd  1245  syl3an2  1305  syl3an3  1306  3jao  1335  biimp3ar  1380  poxp  6376  tfrlemibxssdm  6471  tfr1onlembxssdm  6487  tfrcllembxssdm  6500  nndi  6630  nnmass  6631  pr2nelem  7360  xnn0lenn0nn0  10057  difelfzle  10326  fzo1fzo0n0  10379  elfzo0z  10380  fzofzim  10384  elfzodifsumelfzo  10402  mulexp  10795  expadd  10798  expmul  10801  bernneq  10877  facdiv  10955  pfxfv  11211  swrdswrdlem  11231  pfxccat3  11261  reuccatpfxs1lem  11273  dvdsaddre2b  12347  addmodlteqALT  12365  ltoddhalfle  12399  halfleoddlt  12400  dfgcd2  12530  cncongr1  12620  oddprmgt2  12651  prmfac1  12669  infpnlem1  12877  dfgrp3me  13628  mulgaddcom  13678  mulginvcom  13679  fiinopn  14672  opnneissb  14823  blssps  15095  blss  15096  gausslemma2dlem1a  15731  2sqlem10  15798  ausgrumgrien  15962  ausgrusgrien  15963  ushgredgedg  16018  ushgredgedgloop  16020