Theorem 3imp 1195

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 982	. 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 980

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 982

This theorem is referenced by:  3impa  1196  3imp31  1198  3imp231  1199  3impb  1201  3impia  1202  3impib  1203  3com23  1211  3an1rs  1221  3imp1  1222  3impd  1223  syl3an2  1283  syl3an3  1284  3jao  1312  biimp3ar  1357  poxp  6299  tfrlemibxssdm  6394  tfr1onlembxssdm  6410  tfrcllembxssdm  6423  nndi  6553  nnmass  6554  pr2nelem  7270  xnn0lenn0nn0  9957  difelfzle  10226  fzo1fzo0n0  10276  elfzo0z  10277  fzofzim  10281  elfzodifsumelfzo  10294  mulexp  10687  expadd  10690  expmul  10693  bernneq  10769  facdiv  10847  dvdsaddre2b  12023  addmodlteqALT  12041  ltoddhalfle  12075  halfleoddlt  12076  dfgcd2  12206  cncongr1  12296  oddprmgt2  12327  prmfac1  12345  infpnlem1  12553  dfgrp3me  13302  mulgaddcom  13352  mulginvcom  13353  fiinopn  14324  opnneissb  14475  blssps  14747  blss  14748  gausslemma2dlem1a  15383  2sqlem10  15450