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  6287  tfrlemibxssdm  6382  tfr1onlembxssdm  6398  tfrcllembxssdm  6411  nndi  6541  nnmass  6542  pr2nelem  7253  xnn0lenn0nn0  9934  difelfzle  10203  fzo1fzo0n0  10253  elfzo0z  10254  fzofzim  10258  elfzodifsumelfzo  10271  mulexp  10652  expadd  10655  expmul  10658  bernneq  10734  facdiv  10812  dvdsaddre2b  11987  addmodlteqALT  12004  ltoddhalfle  12037  halfleoddlt  12038  dfgcd2  12154  cncongr1  12244  oddprmgt2  12275  prmfac1  12293  infpnlem1  12500  dfgrp3me  13175  mulgaddcom  13219  mulginvcom  13220  fiinopn  14183  opnneissb  14334  blssps  14606  blss  14607  gausslemma2dlem1a  15215  2sqlem10  15282